Higher-order Horn clauses

DOI10.1145/96559.96570MaRDI QIDQ3495673zbMATH OpenOpenAlexFDO

Authors Gopalan Nadathur, Dale 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)

Recommendations

• scientific article; zbMATH DE number 3988745
• A semantics for Prolog
• scientific article; zbMATH DE number 3992920

Cited in

(33)

• On the algebraic structure of declarative programming languages
• Horn clause programs with polymorphic types: Semantics and resolution
• Graph-based proof procedures for horn clauses
• Unification under a mixed prefix
• Theory of logic programming. An elementary introduction
• Unification with extended patterns
• Horn programming with built-in predicates
• Implementing tactics and tacticals in a higher-order logic programming language
• A proof procedure for the logic of hereditary Harrop formulas
• A semantics for Prolog
• A new framework for declarative programming
• Cut-elimination for a logic with definitions and induction
• Uniform proofs as a foundation for logic programming
• scientific article; zbMATH DE number 1692894 (Why is no real title available?)
• Higher-order logic learning and Progol
• Higher-order quantification and proof search
• A treatment of higher-order features in logic programming
• Proof-theoretic and higher-order extensions of logic programming
• scientific article; zbMATH DE number 3988745 (Why is no real title available?)
• HORNLOG: A graph-based interpreter for general Horn clauses
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)
• scientific article; zbMATH DE number 1497833 (Why is no real title available?)
• scientific article; zbMATH DE number 1508924 (Why is no real title available?)
• A pragmatic reconstruction of λProlog
• scientific article; zbMATH DE number 3992920 (Why is no real title available?)
• Encryption as an abstract data-type (extended abstract)
• A survey of GCLA: a definitional approach to logic programming
• Logic Based Program Synthesis and Transformation
• The Clausal Theory of Types
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• HoCHC: a refutationally complete and semantically invariant system of higher-order logic modulo theories
• Two applications of logic programming to Coq
• Is observational congruence on \(\mu \)-expressions axiomatisable in equational Horn logic?

This page was built for publication: Higher-order Horn clauses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3495673)