Superposition theorem proving for abelian groups represented as integer modules

DOI10.1016/S0304-3975(98)00082-6zbMath0912.68187MaRDI QIDQ1275020

Jürgen Stuber

Publication date: 12 January 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

abelian groupssuperpositionautomated theorem provingparamodulationordering restrictions

Mathematics Subject Classification ID

Related Items

On First-Order Model-Based Reasoning, Superposition with completely built-in abelian groups, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Automatic decidability and combinability, Combinable Extensions of Abelian Groups, Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• NQTHM

Cites Work

• Termination orderings for associative-commutative rewriting systems
• Buchberger's algorithm: The term rewriter's point of view
• Basic paramodulation
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Complete Sets of Reductions for Some Equational Theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Theorem proving in cancellative abelian monoids (extended abstract)
• A precedence-based total AC-compatible ordering
• AC-complete unification and its application to theorem proving
• Associative-commutative deduction with constraints
• AC-superposition with constraints: No AC-unifiers needed
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item