Redundancy criteria for constrained completion

DOI10.1016/0304-3975(94)00274-6zbMath0873.68189OpenAlexW2091691231MaRDI QIDQ673620

Juan-Miguel Gracia

Publication date: 28 February 1997

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

Full work available at URL: https://doi.org/10.1016/0304-3975(94)00274-6

zbMATH Keywords

inference systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (5)

Rewrite semantics for production rule systems: Theory and applications ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ Local simplification ⋮ Local simplification

Cites Work

• Using forcing to prove completeness of resolution and paramodulation
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• A proof theory for general unification
• Unnecessary inferences in associative-commutative completion procedures
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Proving refutational completeness of theorem-proving strategies
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Consider only general superpositions in completion procedures
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Redundancy criteria for constrained completion