Graduate studies at Western
|Abstract||Uniform proofs systems have recently been proposed [Mi191j as a proof-theoretic foundation and generalization of logic programming. In [Mom92a] an extension with constructive negation is presented preserving the nature of abstract logic programming language. Here we adapt this approach to provide a complete theorem proving technique for minimal, intuitionistic and classical logic, which is totally goal-oriented and does not require any form of ancestry resolution. The key idea is to use the Godel-Gentzen translation to embed those logics in the syntax of Hereditary Harrop formulae, for which uniform proofs are complete. We discuss some preliminary implementation issues.|
|Keywords||No keywords specified (fix it)|
No categories specified
(categorize this paper)
|Through your library||Only published papers are available at libraries|
Similar books and articles
Hiroakira Ono (1986). Craig's Interpolation Theorem for the Intuitionistic Logic and its Extensions—a Semantical Approach. Studia Logica 45 (1):19 - 33.
Christoph Kreitz & Brigitte Pientka (2001). Connection-Driven Inductive Theorem Proving. Studia Logica 69 (2):293-326.
Mateja Jamnik, Alan Bundy & Ian Green (1999). On Automating Diagrammatic Proofs of Arithmetic Arguments. Journal of Logic, Language and Information 8 (3):297-321.
Martin Frické Frické (2012). Best-Path Theorem Proving: Compiling Derivations. In James Maclaurin (ed.), Rationis Defensor.
Harold T. Hodes (1983). More About Uniform Upper Bounds on Ideals of Turing Degrees. Journal of Symbolic Logic 48 (2):441-457.
N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
Dale A. Miller (1987). A Compact Representation of Proofs. Studia Logica 46 (4):347 - 370.
Ricardo Caferra, Stéphane Demri & Michel Herment (1993). A Framework for the Transfer of Proofs, Lemmas and Strategies From Classical to Non Classical Logics. Studia Logica 52 (2):197 - 232.
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Alexander Paseau (2011). Proofs of the Compactness Theorem. History and Philosophy of Logic 31 (1):73-98.
Wilfried Sieg & John Byrnes (1998). Normal Natural Deduction Proofs (in Classical Logic). Studia Logica 60 (1):67-106.
David Basin, Seán Matthews & Luca Viganò (1998). Natural Deduction for Non-Classical Logics. Studia Logica 60 (1):119-160.
Sorry, there are not enough data points to plot this chart.
Added to index2010-12-22
Recent downloads (6 months)0
How can I increase my downloads?