Substitution tree indexing

DOI10.1007/3-540-59200-8_52zbMath1503.68291OpenAlexW1560857865MaRDI QIDQ5055823

No author found.

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)

Related Items (13)

Substitution tree indexing ⋮ OpenMP Implementation of Parallel Longest Common Subsequence Algorithm for Mathematical Expression Retrieval ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Engineering DPLL(T) + Saturation ⋮ SPASS & FLOTTER version 0.42 ⋮ Advanced indexing operations on substitution trees ⋮ Path indexing for AC-theories ⋮ Efficient instance retrieval with standard and relational path indexing ⋮ Restricted combinatory unification ⋮ Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ An efficient subsumption test pipeline for BS(LRA) clauses

Uses Software

• OTTER

Cites Work

• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Associative-commutative discrimination nets
• Substitution tree indexing
• Extended path-indexing
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item

This page was built for publication: Substitution tree indexing