Term indexing
First-order terms are widely used in several disciplines of computer science such as term rewriting systems, symbolic computations, logic and functional programming, deductive databases. Therefore there is a need for fast algorithms to manipulate terms. This problem can be formulated abstractly as follows. Given a set \(L\) of terms (called the set of indexed terms), a binary relation R over terms (called the retrieval condition) and a term \(t\) (called the query term), identify the subset \(M\) of \(L\) consisting of all the terms \(l\) such that \(R(l, t)\) holds. The most common examples of retrieval conditions are unification, matching, subsumption. The paper gives detailed description of the term indexing techniques. It is shown how term indexing can be formulated in terms of string matching. This allows to consider many indexing methods as instances of the generic framework.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
- First order Stålmarck. Universal lemmas through branch merges
- Limited resource strategy in resolution theorem proving
- Aligning concepts across proof assistant libraries
- Formalization of the resolution calculus for first-order logic
- Machine learning guidance for connection tableaux
- Twee: an equational theorem prover
- A Knuth-Bendix-like ordering for orienting combinator equations
- Subsumption demodulation in first-order theorem proving
- An efficient subsumption test pipeline for BS(LRA) clauses
- A set automaton to locate all pattern matches in a term
- GKC: a reasoning system for large knowledge bases
- Maintenance of datalog materialisations revisited
- A complete superposition calculus for primal grammars
- Efficient instance retrieval with standard and relational path indexing
- Selecting the selection
- E-matching for fun and profit
- Fingerprint indexing for paramodulation and rewriting
- Higher-order term indexing using substitution trees
- Pre-indexed Terms for Prolog
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- Multi-completion with termination tools
- scientific article; zbMATH DE number 1552512 (Why is no real title available?)
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- scientific article; zbMATH DE number 7455734 (Why is no real title available?)
- Adaptive non-linear pattern matching automata
- Building Theorem Provers
- Logic Programming
- Perfect discrimination graphs: indexing terms with integer exponents
- On the saturation of YAGO
- SAT-Inspired Eliminations for Superposition
- SAT-Based Subsumption Resolution
- Adaptive nonlinear pattern matching automata
- Growing Mathlib: maintenance of a large scale mathematical library
- Finding connections via satisfiability solving
- Anti-pattern templates
- Verified path indexing
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- SAT solving for variants of first-order subsumption
- Learning guided automated reasoning: a brief survey
- Use and abuse of instance parameters in the Lean mathematical library.
- Massive unification
- Proof search algorithm in pure logical framework
- Quantifier simplification by unification in SMT
- Combined reasoning by automated cooperation
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)
