Simple and Efficient Clause Subsumption with Feature Vector Indexing
From MaRDI portal
Publication:4913860
DOI10.1007/978-3-642-36675-8_3zbMath1383.68082OpenAlexW1881680935MaRDI QIDQ4913860
Publication date: 16 April 2013
Published in: Automated Reasoning and Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-36675-8_3
Related Items (20)
Implementing Superposition in iProver (System Description) ⋮ ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) ⋮ Ordered Resolution for Coalition Logic ⋮ Aligning concepts across proof assistant libraries ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Unnamed Item ⋮ Engineering DPLL(T) + Saturation ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ : A Resolution-Based Prover for Multimodal K ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Faster, higher, stronger: E 2.3 ⋮ GKC: a reasoning system for large knowledge bases ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ An efficient subsumption test pipeline for BS(LRA) clauses
Uses Software
Cites Work
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Efficient instance retrieval with standard and relational path indexing
- Fingerprint Indexing for Paramodulation and Rewriting
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Engineering DPLL(T) + Saturation
- Self-adjusting binary search trees
- Probability Theory
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Automated Reasoning
- A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Simple and Efficient Clause Subsumption with Feature Vector Indexing
