Theorem proving modulo associativity
From MaRDI portal
Publication:6560183
DOI10.1007/3-540-61377-3_53zbMATH Open1540.03026MaRDI QIDQ6560183FDOQ6560183
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
- 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)
