Horn equational theories and paramodulation

DOI10.1007/BF00248322MaRDI QIDQ1824409zbMATH OpenOpenAlexFDO

Authors Ulrich Furbach, Steffen Hölldobler, Joachim Schreiber

Publication date 1989

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

Full work available at URL https://doi.org/10.1007/bf00248322

zbMATH Keywords

resolutioncompletenessfixpoint semanticsProlognarrowingparamodulationLogic programmingconditional term rewriting systemsequational Logic programming

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Properties of classes of models (03C52) Models of other mathematical theories (03C65)

Recommendations

• Foundations of equational logic programming
• scientific article; zbMATH DE number 67451
• scientific article; zbMATH DE number 1552532
• Efficient deduction in equality Horn logic by Horn-completion
• A theory of complete logic programs with equality

Cites work

• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 3930372 (Why is no real title available?)
• scientific article; zbMATH DE number 4022665 (Why is no real title available?)
• scientific article; zbMATH DE number 4045129 (Why is no real title available?)
• scientific article; zbMATH DE number 4053008 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3444822 (Why is no real title available?)
• scientific article; zbMATH DE number 3278281 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A theory of complete logic programs with equality
• An Efficient Unification Algorithm
• Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
• Contributions to the Theory of Logic Programming
• Equality, types, modules, and (why not?) generics for logic programming
• Extending SLD resolution to equational horn clauses using E-unification
• Incorporating equality into logic programming via surface deduction
• Oriented equational clauses as a programming language
• Proving Theorems with the Modification Method
• The Concept of Demodulation in Theorem Proving
• The Semantics of Predicate Logic as a Programming Language
• Unit Refutations and Horn Sets

Cited in

(15)

• An intensional epistemic logic
• Equality and abductive residua for Horn clauses
• Incremental constraint satisfaction for equational logic programming
• scientific article; zbMATH DE number 4049137 (Why is no real title available?)
• scientific article; zbMATH DE number 67451 (Why is no real title available?)
• An inference system for horn clause logic with equality
• Oriented equational clauses as a programming language
• scientific article; zbMATH DE number 4022665 (Why is no real title available?)
• Extending SLD resolution to equational horn clauses using E-unification
• Foundations of equational logic programming
• Efficient encodings of first-order Horn formulas in equational logic
• Conditional equational theories and complete sets of transformations
• Theory and Applications of Satisfiability Testing
• A compositional semantic basis for the analysis of equational Horn programs
• Linear and unit-resulting refutations for Horn theories

This page was built for publication: Horn equational theories and paramodulation

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