The anatomy of vampire. Implementing bottom-up procedures with code trees
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1809861
- Rebuilding a tree from its traversals: a case study of program inversion
- scientific article; zbMATH DE number 400623
- Tree Interpolation in Vampire
- Skeletons from the treecode closet
- Combining top-down and bottom-up techniques in program derivation
- scientific article; zbMATH DE number 1629942
Cites work
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- scientific article; zbMATH DE number 3639144 (Why is no real title available?)
- scientific article; zbMATH DE number 1348471 (Why is no real title available?)
- scientific article; zbMATH DE number 814826 (Why is no real title available?)
- scientific article; zbMATH DE number 3254919 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A basis for deductive database systems
- An implementation of hyper-resolution
- Analyzing logic programs using “prop”-ositional logic programs and a magic wand
- Complexity and related enhancements for automated theorem-proving programs
- Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Integrity constraint checking in stratified databases
- Investigating production system representations for non-combinatorial match
- On the efficiency of subsumption algorithms
- Problems and Experiments for and with Automated Theorem-Proving Programs
- Recursive query processing: The power of logic
- Refutation search for Horn sets by a subgoal-extraction method
- Seventy-five problems for testing automatic theorem provers
Cited in
(18)- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- The logicist manifesto: At long last let logic-based artificial intelligence become a field unto itself
- An efficient subsumption test pipeline for BS(LRA) clauses
- Fast and slow enigmas and parental guidance
- Efficient instance retrieval with standard and relational path indexing
- Merging relational database technology with constraint technology
- First-order temporal verification in practice
- Simplifying proofs in Fitch-style natural deduction systems
- A new Gödelian argument for hypercomputing minds based on the busy beaver problem
- scientific article; zbMATH DE number 7455734 (Why is no real title available?)
- Evaluating general purpose automated theorem proving systems
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 7471681 (Why is no real title available?)
- Adaptive nonlinear pattern matching automata
- Deciding Boolean algebra with Presburger arithmetic
- Term ordering diagrams
- Multi-completion with termination tools
- Combining induction and saturation-based theorem proving
This page was built for publication: The anatomy of vampire. Implementing bottom-up procedures with code trees
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1904404)
