Positive deduction modulo regular theories
From MaRDI portal
Publication:6560184
DOI10.1007/3-540-61377-3_54zbMATH Open1540.03027MaRDI QIDQ6560184
Publication date: 21 June 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- Unnamed Item
- Theorem-proving with resolution and superposition
- Completion for rewriting modulo a congruence
- Automated deduction with associative-commutative operators
- Basic paramodulation
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Completion of a Set of Rules Modulo a Set of Equations
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- Proving Theorems with the Modification Method
- Proving refutational completeness of theorem-proving strategies
- A precedence-based total AC-compatible ordering
- Extension of the associative path ordering to a chain of associative commutative symbols
- Associative-commutative deduction with constraints
- A Machine-Oriented Logic Based on the Resolution Principle
- On restrictions of ordered paramodulation with simplification
This page was built for publication: Positive deduction modulo regular theories
