I 38100 Trento \Gamma Loc. Pant' e di Povo \Gamma tel. 0461\Gamma814444 Telex ...  @ NUS Home/Search
Context
Related
| 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 |
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.