Cancellative Abelian monoids and related structures in refutational theorem proving. II

DOI10.1006/jsco.2002.0537zbMath1010.68167OpenAlexW3168074085MaRDI QIDQ1864899

Uwe Waldmann

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.0537

zbMATH Keywords

AC-superposition calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Semigroups (20M99)

Related Items

Extending reduction orderings to ACU-compatible reduction orderings, Cancellative Abelian monoids and related structures in refutational theorem proving. I

Uses Software

• SPASS
• FLOTTER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Extending reduction orderings to ACU-compatible reduction orderings
• Theorem-proving with resolution and superposition
• A general refutational completeness result for an inference procedure based on associative-commutative unification
• Which of the cancellative semigroups are groups?
• Automated deduction with associative-commutative operators
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Proving refutational completeness of theorem-proving strategies
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SPASS & FLOTTER version 0.42
• Theorem proving in cancellative abelian monoids (extended abstract)
• Superposition theorem proving for abelian groups represented as integer modules
• Ordered chaining for total orderings
• Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets