Experiments with discrimination-tree indexing and path indexing for term retrieval

DOI10.1007/BF00245458zbMath0781.68101OpenAlexW2074679569MaRDI QIDQ688554

William W. McCune

Publication date: 20 December 1993

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00245458

zbMATH Keywords

indexingdiscriminationautomated deductionFPA indexingpath indexing

Mathematics Subject Classification ID

Related Items (26)

The higher-order prover \textsc{Leo}-II ⋮ Fast and slow enigmas and parental guidance ⋮ Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures ⋮ Substitution tree indexing ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ The anatomy of vampire. Implementing bottom-up procedures with code trees ⋮ Multi-completion with termination tools ⋮ Model evolution with equality -- revised and implemented ⋮ An algorithm for the retrieval of unifiers from discrimination trees ⋮ Unnamed Item ⋮ Unnamed Item ⋮ LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) ⋮ Advanced indexing operations on substitution trees ⋮ Path indexing for AC-theories ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ MACE4 and SEM: A Comparison of Finite Model Generators ⋮ Citius altius fortius ⋮ Efficient instance retrieval with standard and relational path indexing ⋮ Perfect Discrimination Graphs: Indexing Terms with Integer Exponents ⋮ Extended path-indexing ⋮ FDR explorer ⋮ Faster, higher, stronger: E 2.3 ⋮ Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ Automated proofs of equality problems in Overbeek's competition ⋮ A complete superposition calculus for primal grammars

Uses Software

• OTTER

Cites Work

• Complexity and related enhancements for automated theorem-proving programs
• A New Class of Automated Theorem-Proving Algorithms
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Experiments with discrimination-tree indexing and path indexing for term retrieval