Superposition with completely built-in abelian groups

DOI10.1016/S0747-7171(03)00070-1zbMath1043.03011MaRDI QIDQ1432887

Robert Nieuwenhuis, Guillem Godoy

Publication date: 22 June 2004

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

unificationautomated theorem provingsuperposition with first-order clauses

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items (4)

Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Automatic decidability and combinability ⋮ Combinable Extensions of Abelian Groups ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Superposition theorem proving for abelian groups represented as integer modules
• Decidability and complexity analysis by basic paramodulation
• Paramodulation with built-in AC-theories and symbolic constraints
• Theorem proving with ordering and equality constrained clauses
• Basic paramodulation
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Complete Sets of Reductions for Some Equational Theories
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Theorem proving in cancellative abelian monoids (extended abstract)
• A case study of completion modulo distributivity and Abelian groups
• Associative-commutative deduction with constraints

This page was built for publication: Superposition with completely built-in abelian groups