Theorem proving via uniform proofs

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."