Term indexing
From MaRDI portal
Recommendations
Cited in
(46)- 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)
