Istituto per la Ricerca Scientifica e Tecnologica  (Make Corrections)  
I 38100 Trento \Gamma Loc. Pant' e di Povo \Gamma tel. 0461\Gamma814444 Telex ...

 @ NUS   Home/Search   Context   Related

 
View or download:
sra.itc.it/tr/ACV93.ps.gz
Cached:  PS.gz  PS  PDF  Image  Update  Help

From:  sra.itc.it/?id_...one=5&year=1993 (more)
(Enter author homepages)

Rate this article: (best)
  Comment on this article  
(Enter summary)

Abstract: This paper describes how "safe" proof strategies are represented and executed in the interactive theorem prover GETFOL. A formal metatheory (MT) describes and allows to reason about object level inference. A class of MT terms, called logic tactics, is used to represent proof strategies. The semantic attachment facility and the evaluation mechanism of the GETFOL system have been used to provide the procedural interpretation of logic tactics. The execution of logic tactics is then proved to ... (Update)

Active bibliography (related documents):   More   All
1.5:   Building and Executing Proof Strategies in a Formal Metatheory - Armando, al. (1993)   (Correct)
0.4:   Introspective Metatheoretic Reasoning - Giunchiglia, Cimatti (1994)   (Correct)
0.4:   Program Tactics and Logic Tactics - Giunchiglia, Traverso (1994)   (Correct)

Similar documents based on text:   More   All
0.7:   Multi-Agent Reasoning with Belief Contexts: the Approach and a .. - Cimatti, al. (1994)   (Correct)
0.7:   Multi-Agent Reasoning with Belief Contexts III: Towards the.. - Cimatti (1995)   (Correct)
0.6:   Metatheories About Provability and Metatheories About.. - Serafini, Traverso   (Correct)

BibTeX entry:   (Update)

@misc{ loc-istituto,
  author = "Trento Gamma Loc",
  title = "Istituto per la Ricerca Scientifica e Tecnologica",
  url = "citeseer.comp.nus.edu.sg/712351.html" }
Citations (may not include all citations):
634   A Machine oriented Logic Based on the resolution principle (context) - Robinson - 1965
505   Implementing Mathematics with the NuPRL Proof Development Sy.. - Constable, Allen et al. - 1986
392   A Computational Logic (context) - Boyer, Moore - 1979
167   Natural Deduction - A proof theoretical study (context) - Prawitz - 1965
150   Edinburgh LCF - A mechanized logic of computation (context) - Gordon, Milner et al. - 1979
129   The Foundation of a Generic Theorem Prover - Paulson - 1989
121   Prolegomena to a Theory of Mechanized Formal Reasoning (context) - Weyhrauch - 1980
94   A deductive approach to program synthesis (context) - Manna, Waldinger - 1980
73   Theorem Proving via General Matings (context) - Andrews - 1981
69   On Matrices with Connections (context) - Bibel - 1981
43   A Many Sorted Calculus Based on Resolution and Paramodulatio.. (context) - Walther - 1987
36   The GETFOL Manual - GETFOL version (context) - Giunchiglia - 1992
28   A Metalanguage for Interactive Proof in LCF (context) - Gordon, Milner et al. - 1977
25   Reflective reasoning with and between a declarative metatheo.. - Giunchiglia, Traverso - 1991
23   Embedding Complex Decision Procedures inside an Interactive .. (context) - Armando, Giunchiglia - 1993
20   The Mathematical Language AUTOMATH (context) - deBruijn - 1970
19   A Metatheory of a Mechanized Object Theory - Giunchiglia, Traverso - 1992
14   Introspective Metatheoretic Reasoning - Giunchiglia, Cimatti - 1992
13   Program tactics and logic tactics - Giunchiglia, Traverso - 1993
9   A System for Multi-Level Reasoning (context) - Giunchiglia, Traverso et al. - 1992
9   GETFOL User Manual - GETFOL version (context) - Giunchiglia, Traverso - 1991
5   A Conceptual Architecture for Introspective Systems (context) - Giunchiglia, Armando - 1993
4   HGKM User Manual - HGKM version (context) - Giunchiglia, Cimatti - 1991
3   Introspective Metatheoretic Theorem Proving (context) - Giunchiglia, Cimatti - 1992

Documents on the same site (http://sra.itc.it/?id_menu=19&id_sezione=5&year=1993):   More
A General Purpose Reasoner for Abstraction - Giunchiglia, al. (1993)   (Correct)
Istituto per la Ricerca Scientifica e Tecnologica - Trento Gamma Loc   (Correct)
Structured Proof Procedures - Giunchiglia, Armando, Pecchiari (1993)   (Correct)

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.