Substitution tree indexing

DOI10.1007/3-540-59200-8_52MaRDI QIDQ5055823zbMATH OpenOpenAlexFDO

Authors

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-59200-8_52

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Advanced indexing operations on substitution trees
• Logic Programming
• Fast term indexing with coded context trees
• scientific article; zbMATH DE number 1765673
• scientific article; zbMATH DE number 1552512

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Associative-commutative discrimination nets
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Extended path-indexing
• scientific article; zbMATH DE number 3684930 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Otter 2.0
• Substitution tree indexing

Cited in

(25)

• Fast term indexing with coded context trees
• A Knuth-Bendix-like ordering for orienting combinator equations
• An efficient subsumption test pipeline for BS(LRA) clauses
• Restricted combinatory unification
• Efficient instance retrieval with standard and relational path indexing
• Term indexing
• Fingerprint indexing for paramodulation and rewriting
• Higher-order term indexing using substitution trees
• Engineering DPLL(T) + Saturation
• scientific article; zbMATH DE number 1552512 (Why is no real title available?)
• scientific article; zbMATH DE number 1765673 (Why is no real title available?)
• SPASS \& FLOTTER version 0.42
• Advanced indexing operations on substitution trees
• Path indexing for AC-theories
• scientific article; zbMATH DE number 7455734 (Why is no real title available?)
• Adaptive non-linear pattern matching automata
• Substitution tree indexing
• OpenMP implementation of parallel longest common subsequence algorithm for mathematical expression retrieval
• Logic Programming
• Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses
• Perfect discrimination graphs: indexing terms with integer exponents
• Examination of the state of the art of mathematical formula search for zbMATH Open
• Merging relational database technology with constraint technology
• Adaptive nonlinear pattern matching automata
• Experiments with discrimination-tree indexing and path indexing for term retrieval

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: Substitution tree indexing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055823)