Uniform proofs as a foundation for logic programming (Q2640596)

Cut-free Gentzen-type systems for first and second order classical, intuitionistic and minimal logic are considered. A uniform proof is a derivation in which (viewed bottom-up) a succedent rule is applied whenever possible: if the succedent of a sequent S is non-atomic, then S is a conclusion of the succedent rule. If uniform proofs are complete for a class of sequents, then the proof-search for this class can be done in goal-directed manner by analysing non-atomic goals and expanding atomic goals using unification in a PROLOG-like manner. This justifies the definition of an abstract logic programming language as a triple \(<{\mathcal D},{\mathcal G}>\) such that uniform intuitionistic proofs are complete for the sequents \(X\to G\) with finite \(X\subset {\mathcal D}\) and G in \({\mathcal G}\). Four abstract logic programming languages are considered. First order Horn clauses \({\mathcal H}_ 1\) (with a definition equivalent to the familiar one up to equivalence), higher order Horn clauses \({\mathcal H}_ 2\), first and higher order hereditary Harrop formulas \({\mathcal D}_ 3\) and \({\mathcal D}_ 4\) (with suitable definitions of goals). \({\mathcal H}_ 1\), \({\mathcal H}_ 2\) are Glivenko classes (i.e. classical validity of \(X\to G\) in the corresponding language implies intuitionistic derivability), while \({\mathcal D}_ 3\), \({\mathcal D}_ 4\) are not. \({\mathcal H}_ 1\) is Herbrand universe for \({\mathcal H}_ 2\), and \({\mathcal H}_ 2\) is Herbrand universe for \({\mathcal D}_ 4\), i.e. it is sufficient to use the \(\lambda\)- abstraction of formulas in \({\mathcal H}_ 1\), \({\mathcal H}_ 2\) in substitutions for higher order quantifiers. A survey of implemented applications of this approach seems to show that they are more diverse than known applications of other systems based on automatic or interactive proofs in higher order intuitionistic logic.