scientific article; zbMATH DE number 3988745

MaRDI QIDQ3751042zbMATH OpenFDO

Authors Gopalan Nadathur, Dale Miller

Publication date 1986

zbMATH Keywords

definite clauseshigher-order unificationHorn-clause programslogic programmingPROLOG-type interpreterundecidability

Mathematics Subject Classification ID

Recommendations

• Higher-order Horn clauses
• The Clausal Theory of Types
• scientific article; zbMATH DE number 3992920
• Uniform proofs as a foundation for logic programming

Cited in

(31)

• A unification algorithm for second-order monadic terms
• Horn clause programs with polymorphic types: Semantics and resolution
• A semantics for Prolog
• Making PVS accessible to generic services by interpretation in a universal format
• Mechanized metatheory revisited
• Uniform proofs as a foundation for logic programming
• scientific article; zbMATH DE number 1638651 (Why is no real title available?)
• Encoding generic judgments: preliminary results
• Programming with higher-order logic.
• Higher-order quantification and proof search
• Coalgebraic semantics for parallel derivation strategies in logic programming
• Refinement of Higher-Order Logic Programs
• Higher-order Horn clauses
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)
• HiLog: A foundation for higher-order logic programming
• scientific article; zbMATH DE number 1255555 (Why is no real title available?)
• scientific article; zbMATH DE number 1028827 (Why is no real title available?)
• scientific article; zbMATH DE number 3992920 (Why is no real title available?)
• scientific article; zbMATH DE number 2090533 (Why is no real title available?)
• Logic programs with equational type specifications
• The expressive power of higher-order Datalog
• Implementing type theory in higher order constraint logic programming
• Reasoning with higher-order abstract syntax in a logical framework
• The Clausal Theory of Types
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• Higher order E-unification
• HoCHC: a refutationally complete and semantically invariant system of higher-order logic modulo theories
• The relational machine calculus
• Types, Tableaus and Gödel’s God in Isabelle/HOL
• Simple second-order languages for which unification is undecidable
• Expressing combinatory reduction systems derivations in the rewriting calculus

This page was built for publication:

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