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

DOI10.1007/BF00245458zbMATH Open0781.68101OpenAlexW2074679569MaRDI QIDQ688554FDOQ688554

William 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

Recommendations

• Term indexing
• scientific article; zbMATH DE number 1552512
• Substitution tree indexing
• Extended path-indexing
• Fast term indexing with coded context trees

zbMATH Keywords

automated deductiondiscriminationindexingFPA indexingpath indexing

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Complexity and related enhancements for automated theorem-proving programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• A New Class of Automated Theorem-Proving Algorithms

Cited In (29)

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

Uses Software

• OTTER

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

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