On narrowing, refutation proofs and constraints

DOI10.1007/3-540-59200-8_47zbMath1503.03019OpenAlexW1576882193MaRDI QIDQ5055818

Robert Nieuwenhuis

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-59200-8_47

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Decidability and complexity analysis by basic paramodulation

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Narrowing vs. SLD-resolution
• Foundations of equational logic programming
• Basic narrowing revisited
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• A precedence-based total AC-compatible ordering
• Associative-commutative deduction with constraints
• AC-superposition with constraints: No AC-unifiers needed
• An optimal narrowing strategy for general canonical systems
• Completion of first-order clauses with equality by strict superposition