Term indexing
From MaRDI portal
Recommendations
Cited in
(39)- Higher-order term indexing using substitution trees
- Logic Programming
- Building Theorem Provers
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- An efficient subsumption test pipeline for BS(LRA) clauses
- Quantifier simplification by unification in SMT
- GKC: a reasoning system for large knowledge bases
- First order Stålmarck. Universal lemmas through branch merges
- A set automaton to locate all pattern matches in a term
- Efficient instance retrieval with standard and relational path indexing
- Aligning concepts across proof assistant libraries
- Formalization of the resolution calculus for first-order logic
- Fingerprint indexing for paramodulation and rewriting
- Maintenance of datalog materialisations revisited
- A complete superposition calculus for primal grammars
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Selecting the selection
- Machine learning guidance for connection tableaux
- Combined reasoning by automated cooperation
- Learning guided automated reasoning: a brief survey
- Use and abuse of instance parameters in the Lean mathematical library.
- Pre-indexed Terms for Prolog
- Subsumption demodulation in first-order theorem proving
- scientific article; zbMATH DE number 7455734 (Why is no real title available?)
- On the saturation of YAGO
- scientific article; zbMATH DE number 7471681 (Why is no real title available?)
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Twee: an equational theorem prover
- Limited resource strategy in resolution theorem proving
- scientific article; zbMATH DE number 1552512 (Why is no real title available?)
- Proof search algorithm in pure logical framework
- Multi-completion with termination tools
- SAT-Based Subsumption Resolution
- Perfect discrimination graphs: indexing terms with integer exponents
- E-matching for fun and profit
- SAT-Inspired Eliminations for Superposition
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- A Knuth-Bendix-like ordering for orienting combinator equations
This page was built for publication: Term indexing
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751378)
