Simple and Efficient Clause Subsumption with Feature Vector Indexing
From MaRDI portal
Recommendations
- Theory and Applications of Satisfiability Testing
- Higher-order term indexing using substitution trees
- A formal approach to subgrammar extraction for NLP
- scientific article; zbMATH DE number 1931822
- Encoding Redundancy for Satisfaction-Driven Clause Learning
- Efficient all-UIP learned clause minimization
Cites work
- A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
- Automated Reasoning
- Combining superposition, sorts and splitting
- Efficient instance retrieval with standard and relational path indexing
- Engineering DPLL(T) + Saturation
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Fingerprint indexing for paramodulation and rewriting
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 1809863 (Why is no real title available?)
- scientific article; zbMATH DE number 4049047 (Why is no real title available?)
- scientific article; zbMATH DE number 1552512 (Why is no real title available?)
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Probability Theory
- Self-adjusting binary search trees
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Term indexing
- The anatomy of vampire. Implementing bottom-up procedures with code trees
Cited in
(24)- 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
- \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Automata-driven indexing of prolog clauses
- Ordered resolution for coalition logic
- Engineering DPLL(T) + Saturation
- 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
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- scientific article; zbMATH DE number 7806140 (Why is no real title available?)
- SAT-Based Subsumption Resolution
- Extending a high-performance prover to higher-order logic
- SAT solving for variants of first-order subsumption
Describes a project that uses
Uses Software
This page was built for publication: Simple and Efficient Clause Subsumption with Feature Vector Indexing
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4913860)
