Conditional equational theories and complete sets of transformations

DOI10.1016/0304-3975(90)90063-NzbMath0706.03028OpenAlexW2001661991MaRDI QIDQ918541

Steffen Hölldobler

Publication date: 1990

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(90)90063-n

zbMATH Keywords

reflectionHerbrand modelparamodulationcomplete sets of transformationsconditional equational theoriessearch space

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Equational classes, universal algebra in model theory (03C05)

Related Items (1)

Incremental constraint satisfaction for equational logic programming

Uses Software

• NARROWER

Cites Work

• Closures and fairness in the semantics of programming logic
• Conditional rewrite rules
• Modelling the combination of functional and logic programming languages
• Incorporating equality into logic programming via surface deduction
• Conditional rewrite rules: Confluence and termination
• Unification theory
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Complete sets of transformations for general E-unification
• Foundations of equational logic programming
• Higher-order unification revisited: Complete sets of transformations
• Horn equational theories and paramodulation
• Basic narrowing revisited
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Oriented equational clauses as a programming language
• The relation between logic and functional languages: a survey
• Extending SLD resolution to equational horn clauses using E-unification
• Proving termination with multiset orderings
• An Efficient Unification Algorithm
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• The undecidability of unification in third order logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Conditional equational theories and complete sets of transformations