Superposition theorem proving for commutative rings

MaRDI QIDQ2702595zbMATH OpenFDO

Authors Jürgen Stuber

Publication date 21 October 2001

zbMATH Keywords

automated theorem provingcommutative ringssuperposition calculusterm rewriting system

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Applications of logic to commutative algebra (13L05) Computational aspects and applications of commutative rings (13P99) Grammars and rewriting systems (68Q42)

Recommendations

• Superposition theorem proving for abelian groups represented as integer modules
• Superposition theorem proving for abelian groups represented as integer modules
• Automated proof of ring commutativity problems by algebraic methods
• Automated deduction in ring theory
• Automated reasoning in reduction rings using the Theorema system

Cited in

(2)

• Superposition theorem proving for abelian groups represented as integer modules
• Harald Ganzinger's legacy: contributions to logics and programming

This page was built for publication: Superposition theorem proving for commutative rings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2702595)