SAT-Based Subsumption Resolution

DOI10.1007/978-3-031-38499-8_11MaRDI QIDQ6492740zbMATH OpenFDO

Authors Laura Kovács, Michael G. Rawson, Jakob Rath

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• AVATAR: The Architecture for First-Order Theorem Provers
• Faster, higher, stronger: E 2.3
• scientific article; zbMATH DE number 4049047 (Why is no real title available?)
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Paramodulation-based theorem proving
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Subsumption demodulation in first-order theorem proving
• Term indexing
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

Cited in

(2)

• Finding connections via satisfiability solving
• SAT solving for variants of first-order subsumption

This page was built for publication: SAT-Based Subsumption Resolution

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