AC simplifications and closure redundancies in the superposition calculus

DOI10.1007/978-3-030-86059-2_12OpenAlexW3204421122MaRDI QIDQ2142076

André Duarte, Konstantin Korovin

Publication date: 25 May 2022

Full work available at URL: https://arxiv.org/abs/2107.08409

zbMATH Keywords

superpositiondemodulationfirst-order theorem provingground joinabilityassociativity-commutativityiProver

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

AC simplifications and closure redundancies in the superposition calculus ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Ground joinability and connectedness in the superposition calculus

Uses Software

• VAMPIRE
• SPASS
• TPTP
• iProver
• E Theorem Prover
• Waldmeister
• MadMax
• Twee

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On using ground joinable equations in equational theorem proving
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• MædMax: a maximal ordered completion tool
• Basic paramodulation
• Twee: an equational theorem prover
• AC simplifications and closure redundancies in the superposition calculus
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Proving termination with multiset orderings
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Term Rewriting and All That
• Implementing Superposition in iProver (System Description)
• Making higher-order superposition work

This page was built for publication: AC simplifications and closure redundancies in the superposition calculus