Simple and Efficient Clause Subsumption with Feature Vector Indexing
From MaRDI portal
Publication:4913860
DOI10.1007/978-3-642-36675-8_3zbMath1383.68082MaRDI 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
03B35: Mechanization of proofs and logical operations
Related Items
Simple and Efficient Clause Subsumption with Feature Vector Indexing, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Implementing Superposition in iProver (System Description), ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), The CADE-28 Automated Theorem Proving System Competition – CASC-28, The CADE-26 automated theorem proving system competition – CASC-26, The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9, Aligning concepts across proof assistant libraries, Set of support, demodulation, paramodulation: a historical perspective, An efficient subsumption test pipeline for BS(LRA) clauses, Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \), \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments, Faster, higher, stronger: E 2.3, GKC: a reasoning system for large knowledge bases, : A Resolution-Based Prover for Multimodal K, Predicate Elimination for Preprocessing in First-Order Theorem Proving, Ordered Resolution for Coalition Logic, Engineering DPLL(T) + Saturation
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
