Horn equational theories and paramodulation

DOI10.1007/BF00248322zbMATH Open0682.68091OpenAlexW1967047591MaRDI QIDQ1824409FDOQ1824409

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

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

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)

Cites Work

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

Cited In (15)

• An intensional epistemic logic
• Equality and abductive residua for Horn clauses
• Incremental constraint satisfaction for equational logic programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• An inference system for horn clause logic with equality
• Oriented equational clauses as a programming language
• Title not available (Why is that?)
• 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)