Carnegie Mellon University
file.pdf (627.31 kB)

Theorem proving via uniform proofs

Download (627.31 kB)
journal contribution
posted on 1993-01-01, 00:00 authored by Alberto Momigliano
Abstract: "Uniform proofs systems have recently been proposed [Mil91] 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 Gödel-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."


Publisher Statement

All Rights Reserved



Usage metrics