file.pdf (627.31 kB)
Theorem proving via uniform proofs
journal contributionposted 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 Go╠ê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."