The anatomy of vampire. Implementing bottom-up procedures with code trees
From MaRDI portal
Publication:1904404
DOI10.1007/BF00881918zbMath0838.68100WikidataQ56429030 ScholiaQ56429030MaRDI QIDQ1904404
Publication date: 20 December 1995
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items
Fast and slow enigmas and parental guidance, First-order temporal verification in practice, Simplifying proofs in Fitch-style natural deduction systems, Deciding Boolean algebra with Presburger arithmetic, Multi-completion with termination tools, Unnamed Item, Unnamed Item, 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, Efficient instance retrieval with standard and relational path indexing, A new Gödelian argument for hypercomputing minds based on the busy beaver problem, Combining induction and saturation-based theorem proving, An efficient subsumption test pipeline for BS(LRA) clauses, Evaluating general purpose automated theorem proving systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Seventy-five problems for testing automatic theorem provers
- Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- Complexity and related enhancements for automated theorem-proving programs
- An implementation of hyper-resolution
- Recursive query processing: The power of logic
- Investigating production system representations for non-combinatorial match
- Analyzing logic programs using “prop”-ositional logic programs and a magic wand
- Refutation search for Horn sets by a subgoal-extraction method
- A basis for deductive database systems
- On the efficiency of subsumption algorithms
- Integrity constraint checking in stratified databases
- Problems and Experiments for and with Automated Theorem-Proving Programs
- A Machine-Oriented Logic Based on the Resolution Principle
