Cancellative Abelian monoids and related structures in refutational theorem proving. I
From MaRDI portal
Recommendations
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- Theorem proving in cancellative abelian monoids (extended abstract)
- scientific article; zbMATH DE number 1303342
- scientific article; zbMATH DE number 1405448
- Superposition theorem proving for abelian groups represented as integer modules
Cites work
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- A Practical Decision Procedure for Arithmetic with Function Symbols
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- AC-complete unification and its application to theorem proving
- AC-superposition with constraints: no AC-unifiers needed
- Associative-commutative deduction with constraints
- Automated deduction with associative-commutative operators
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- Complete Sets of Reductions for Some Equational Theories
- Complexity of unification problems with associative-commutative operators
- scientific article; zbMATH DE number 4053061 (Why is no real title available?)
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- scientific article; zbMATH DE number 46359 (Why is no real title available?)
- scientific article; zbMATH DE number 1140679 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- Normalized rewriting: An alternative to rewriting modulo a set of equations
- Proving refutational completeness of theorem-proving strategies
- Refutational theorem proving for hierarchic first-order theories
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Superposition theorem proving for abelian groups represented as integer modules
- Termination and completion modulo associativity, commutativity and identity
- Termination of rewriting systems by polynomial interpretations and its implementation
- Theorem proving in cancellative abelian monoids (extended abstract)
- Theorem-proving with resolution and superposition
- Using forcing to prove completeness of resolution and paramodulation
Cited in
(9)- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- Theorem proving in cancellative abelian monoids (extended abstract)
- scientific article; zbMATH DE number 1405448 (Why is no real title available?)
- Superposition theorem proving for abelian groups represented as integer modules
- Combinable Extensions of Abelian Groups
- A comprehensive framework for saturation theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
- Levi's commutator theorems for cancellative semigroups.
This page was built for publication: Cancellative Abelian monoids and related structures in refutational theorem proving. I
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1864898)
