A proof procedure for the logic of hereditary Harrop formulas

DOI10.1007/BF00881902zbMath0796.03012MaRDI QIDQ1311397

Gopalan Nadathur

Publication date: 26 September 1994

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

unificationintuitionistic logicproof procedureabstract logic programming languageclause formlogic of hereditary Harrop formulaslogic programming language \(\lambda\)-Prolog

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

The undecidability of proof search when equality is a logical connective, A Survey of the Proof-Theoretic Foundations of Logic Programming, Correct Answers for First Order Logic, Non-commutative proof construction: a constraint-based approach, Representing scope in intuitionistic deductions, On the algebraic structure of declarative programming languages, Correspondences between classical, intuitionistic and uniform provability

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification under a mixed prefix
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Uniform proofs as a foundation for logic programming
• Scoping constructs in logic programming: Implementation problems and their solution
• Higher-order Horn clauses
• Clausal intuitionistic logic II. tableau proof procedures
• An Efficient Unification Algorithm
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The Semantics of Predicate Logic as a Programming Language