Experiments with discrimination-tree indexing and path indexing for term retrieval
From MaRDI portal
Publication:688554
Recommendations
Cites work
- scientific article; zbMATH DE number 3821130 (Why is no real title available?)
- scientific article; zbMATH DE number 3986666 (Why is no real title available?)
- scientific article; zbMATH DE number 3684930 (Why is no real title available?)
- A New Class of Automated Theorem-Proving Algorithms
- Complexity and related enhancements for automated theorem-proving programs
Cited in
(29)- MACE4 and SEM: a comparison of finite model generators
- A complete superposition calculus for primal grammars
- Extended path-indexing
- Faster, higher, stronger: E 2.3
- Path indexing for AC-theories
- Efficient instance retrieval with standard and relational path indexing
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- Fast and slow enigmas and parental guidance
- The higher-order prover \textsc{Leo}-II
- Term indexing
- scientific article; zbMATH DE number 1552512 (Why is no real title available?)
- Substitution tree indexing
- Automated proofs of equality problems in Overbeek's competition
- Multi-completion with termination tools
- Model evolution with equality -- revised and implemented
- Extending a high-performance prover to higher-order logic
- FDR explorer
- An algorithm for the retrieval of unifiers from discrimination trees
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- The application of automated reasoning to questions in mathematics and logic
- scientific article; zbMATH DE number 7471681 (Why is no real title available?)
- An efficient subsumption test pipeline for BS(LRA) clauses
- scientific article; zbMATH DE number 7455734 (Why is no real title available?)
- Advanced indexing operations on substitution trees
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses
- Perfect discrimination graphs: indexing terms with integer exponents
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)
