Theorem Proving via Uniform Proofs>

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,102

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Similar books and articles

On automating diagrammatic proofs of arithmetic arguments.Mateja Jamnik, Alan Bundy & Ian Green - 1999 - Journal of Logic, Language and Information 8 (3):297-321.
Symbolic logic and mechanical theorem proving.Chin-Liang Chang - 1973 - San Diego: Academic Press. Edited by Richard Char-Tung Lee.
More about uniform upper Bounds on ideals of Turing degrees.Harold T. Hodes - 1983 - Journal of Symbolic Logic 48 (2):441-457.
Metamathematics, machines, and Gödel's proof.N. Shankar - 1994 - New York: Cambridge University Press.
A compact representation of proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.
Proofs of the Compactness Theorem.Alexander Paseau - 2010 - History and Philosophy of Logic 31 (1):73-98.

Analytics

Added to PP
2010-12-22

Downloads
13 (#913,759)

6 months
2 (#785,137)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references