A Prolog technology theorem prover: Implementation by an extended Prolog compiler
From MaRDI portal
Publication:1114446
DOI10.1007/BF00297245zbMATH Open0662.68104DBLPjournals/jar/Stickel88WikidataQ56059054 ScholiaQ56059054MaRDI QIDQ1114446FDOQ1114446
Authors: Mark E. Stickel 
Publication date: 1988
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Recommendations
- scientific article; zbMATH DE number 3986671
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- An examination of the prolog technology theorem-prover
- Prolog technology for default reasoning: proof theory and compilation techniques
- Extensions to logic programming motivated by the construction of a generic theorem prover
- An improved proof-theoretic compilation of logic programs
- scientific article; zbMATH DE number 3965464
- scientific article; zbMATH DE number 4053062
- Publication:4945207
- Proof-theoretic and higher-order extensions of logic programming
General topics in the theory of software (68N01) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Cites Work
- Linear resolution with selection function
- A Hole in Goal Trees: Some Guidance from Resolution Theory
- Title not available (Why is that?)
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- Title not available (Why is that?)
- Title not available (Why is that?)
- Depth-first iterative-deepening: An optimal admissible tree search
- Theorem Proving via General Matings
- Non-Horn clause logic programming without contrapositives
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A simplified problem reduction format
- Refutation graphs
- An Implementation of the Model Elimination Proof Procedure
- Experimental tests of resolution-based theorem-proving strategies
- Resolution, Refinements, and Search Strategies: A Comparative Study
- Title not available (Why is that?)
Cited In (64)
- Building Theorem Provers
- Efficient model generation through compilation.
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Compiling a default reasoning system into Prolog
- Tabling, rational terms, and coinduction finally together!
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Unrestricted resolution versus N-resolution
- From Schütte’s Formal Systems to Modern Automated Deduction
- Improving the time efficiency of proving theorems using a learning mechanism
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Avoiding duplicate proofs with the foothold refinement
- An examination of the prolog technology theorem-prover
- Closures and Modules Within Linear Logic Concurrent Constraint Programming
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- Linear resolution for consequence finding
- Mark Stickel: his earliest work
- Semantically-guided goal-sensitive reasoning: model representation
- Non-Horn clause logic programming
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Refinements to depth-first iterative-deepening search in automatic theorem proving
- Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
- Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
- SET-VAR
- SETHEO: A high-performance theorem prover
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Computing answers with model elimination
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Optimizing proof search in model elimination
- Controlled integration of the cut rule into connection tableau calculi
- Title not available (Why is that?)
- IeanCOP: lean connection-based theorem proving
- Title not available (Why is that?)
- IDNAF Prolog
- Title not available (Why is that?)
- Craig interpolation with clausal first-order tableaux
- Problem solving by searching for models with a theorem prover
- Partheo: A high-performance parallel theorem prover
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- A novel asynchronous parallelism scheme for first-order logic
- Subgoal alternation in model elimination
- Efficient model generation through compilation
- A complete semantic back chaining proof system
- A semantic backward chaining proof system
- The application of automated reasoning to questions in mathematics and logic
- History and prospects for first-order automated deduction
- Validation and verification of decision making rules
- Controlled use of clausal lemmas in connection tableau calculi
- The BinProlog experience: architecture and implementation choices for continuation passing Prolog and first-class logic engines
- lean\(T^ AP\): Lean tableau-based deduction
- Prolog Technology Reinforcement Learning Prover
- Title not available (Why is that?)
- Title not available (Why is that?)
- nanoCoP: a non-clausal connection prover
- Logic-based subsumption architecture
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- A Mizar mode for HOL
- Lemma matching for a PTTP-based top-down theorem prover
- Abductive reasoning with a large knowledge base for discourse processing
- A Prolog assisted search for new simple Lie algebras
- Investigations into proof structures
- Lemmas: generation, selection, application
- Range-restricted and Horn interpolation through clausal tableaux
This page was built for publication: A Prolog technology theorem prover: Implementation by an extended Prolog compiler
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1114446)
