Subsumption demodulation in first-order theorem proving

DOI10.1007/978-3-030-51074-9_17OpenAlexW3038385067MaRDI QIDQ2096454

Laura Kovács, Bernhard Gleiss, Jakob Rath

Publication date: 9 November 2022

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

Mathematics Subject Classification ID

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

Related Items (7)

Automated generation of exam sheets for automated deduction ⋮ Unifying splitting ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• VAMPIRE
• SMT-LIB
• SPASS
• TPTP
• z3
• StarExec
• CVC4
• AVATAR
• GNU parallel

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Scaling up DPLL(T) string solvers using context-dependent simplification
• Faster, higher, stronger: E 2.3
• AVATAR: The Architecture for First-Order Theorem Provers
• Horn Clause Solvers for Program Verification
• Subterm contextual rewriting
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• From Search to Computation: Redundancy Criteria and Simplification at Work
• Computer Aided Verification

This page was built for publication: Subsumption demodulation in first-order theorem proving