Higher-order Horn clauses

DOI10.1145/96559.96570zbMath0711.68091OpenAlexW2169526198MaRDI QIDQ3495673

Gopalan Nadathur, Dale A. Miller

Publication date: 1990

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://repository.upenn.edu/cis_reports/847

zbMATH Keywords

higher-order logicHorn clauseslogic programmingprolog

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17)

Related Items

A semantics for \(\lambda \)Prolog ⋮ Uniform proofs as a foundation for logic programming ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ A new framework for declarative programming ⋮ Unification under a mixed prefix ⋮ Encryption as an abstract data-type ⋮ Is observational congruence on \(\mu \)-expressions axiomatisable in equational Horn logic? ⋮ Unification with extended patterns ⋮ On the algebraic structure of declarative programming languages ⋮ Cut-elimination for a logic with definitions and induction ⋮ Implementing tactics and tacticals in a higher-order logic programming language ⋮ A proof procedure for the logic of hereditary Harrop formulas