Local simplification
From MaRDI portal
Publication:1271570
DOI10.1006/inco.1997.2690zbMath0909.68163OpenAlexW2912892936MaRDI QIDQ1271570
Publication date: 10 November 1998
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/cb240fec1d4c2d744acc620df6893414f892a5e9
Cites Work
- Unnamed Item
- Unnamed Item
- Redundancy criteria for constrained completion
- Using forcing to prove completeness of resolution and paramodulation
- Theorem proving with ordering and equality constrained clauses
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Proving refutational completeness of theorem-proving strategies
- Associative-commutative deduction with constraints
- AC-superposition with constraints: No AC-unifiers needed
- The Concept of Demodulation in Theorem Proving
- Mechanical Theorem-Proving by Model Elimination
