SAT-Based Subsumption Resolution
From MaRDI portal
Publication:6492740
DOI10.1007/978-3-031-38499-8_11MaRDI QIDQ6492740
Michael G. Rawson, Author name not available (Why is that?), Laura Kovács, Jakob Rath
Publication date: 26 April 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Subsumption demodulation in first-order theorem proving
- Faster, higher, stronger: E 2.3
- Resolution theorem proving
- Paramodulation-based theorem proving
- Term indexing
- AVATAR: The Architecture for First-Order Theorem Provers
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
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)
