Theorem proving modulo associativity
From MaRDI portal
Publication:6560183
DOI10.1007/3-540-61377-3_53zbMATH Open1540.03026MaRDI QIDQ6560183FDOQ6560183
Authors: Albert Rubio 
Publication date: 21 June 2024
Recommendations
- Equational theorem proving modulo
- Automated deduction with associative-commutative operators
- Associative-commutative deduction with constraints
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- Theorem proving with ordering and equality constrained clauses
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Complete Sets of Reductions for Some Equational Theories
- THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
- Title not available (Why is that?)
- AC-superposition with constraints: no AC-unifiers needed
- Theorem proving with ordering and equality constrained clauses
- Title not available (Why is that?)
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Completion of a Set of Rules Modulo a Set of Equations
- Title not available (Why is that?)
- Any ground associative-commutative theory has a finite canonical system
- A total AC-compatible ordering based on RPO
- Title not available (Why is that?)
- Associative-commutative deduction with constraints
This page was built for publication: Theorem proving modulo associativity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6560183)
