Substitution tree indexing

DOI10.1007/3-540-59200-8_52zbMATH Open1503.68291OpenAlexW1560857865MaRDI QIDQ5055823FDOQ5055823

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

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

Mathematics Subject Classification ID

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

Cites Work

• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Title not available (Why is that?)
• Otter 2.0
• Associative-commutative discrimination nets
• Substitution tree indexing
• Extended path-indexing

Cited In (24)

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

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)