Horn equational theories and paramodulation

DOI10.1007/BF00248322zbMath0682.68091OpenAlexW1967047591MaRDI QIDQ1824409

Joachim Schreiber, Steffen Hölldobler, Ulrich Furbach

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

Logic programmingcompletenessresolutionProlognarrowingfixpoint semanticsparamodulationconditional term rewriting systemsequational Logic programming

Mathematics Subject Classification ID

Related Items (4)

Incremental constraint satisfaction for equational logic programming ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Conditional equational theories and complete sets of transformations ⋮ An intensional epistemic logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Incorporating equality into logic programming via surface deduction
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Oriented equational clauses as a programming language
• A theory of complete logic programs with equality
• Extending SLD resolution to equational horn clauses using E-unification
• An Efficient Unification Algorithm
• Contributions to the Theory of Logic Programming
• Unit Refutations and Horn Sets
• Proving Theorems with the Modification Method
• The Semantics of Predicate Logic as a Programming Language
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving
• Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
• Equality, types, modules, and (why not?) generics for logic programming

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