Cancellative Abelian monoids and related structures in refutational theorem proving. I
From MaRDI portal
Publication:1864898
DOI10.1006/jsco.2002.0536zbMath1010.68166OpenAlexW2765809787MaRDI QIDQ1864898
Publication date: 23 March 2003
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/jsco.2002.0536
Related Items (5)
Combinable Extensions of Abelian Groups ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ A comprehensive framework for saturation theorem proving ⋮ A comprehensive framework for saturation theorem proving ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Termination of rewriting systems by polynomial interpretations and its implementation
- Complexity of unification problems with associative-commutative operators
- Using forcing to prove completeness of resolution and paramodulation
- Theorem-proving with resolution and superposition
- Termination and completion modulo associativity, commutativity and identity
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- Refutational theorem proving for hierarchic first-order theories
- Automated deduction with associative-commutative operators
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- Normalized rewriting: An alternative to rewriting modulo a set of equations
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Complete Sets of Reductions for Some Equational Theories
- A Practical Decision Procedure for Arithmetic with Function Symbols
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Theorem proving in cancellative abelian monoids (extended abstract)
- AC-complete unification and its application to theorem proving
- Superposition theorem proving for abelian groups represented as integer modules
- Associative-commutative deduction with constraints
- AC-superposition with constraints: No AC-unifiers needed
This page was built for publication: Cancellative Abelian monoids and related structures in refutational theorem proving. I
