A Prolog technology theorem prover: Implementation by an extended Prolog compiler
From MaRDI portal
Publication:1114446
DOI10.1007/BF00297245zbMath0662.68104WikidataQ56059054 ScholiaQ56059054MaRDI QIDQ1114446
Publication date: 1988
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) General topics in the theory of software (68N01)
Related Items
IDNAF Prolog, Mark Stickel: his earliest work, Semantically-guided goal-sensitive reasoning: model representation, Problem solving by searching for models with a theorem prover, Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, Prolog Technology Reinforcement Learning Prover, Controlled integration of the cut rule into connection tableau calculi, Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, History and Prospects for First-Order Automated Deduction, The application of automated reasoning to questions in mathematics and logic, A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation, Validation and verification of decision making rules, lean\(T^ AP\): Lean tableau-based deduction, The anatomy of vampire. Implementing bottom-up procedures with code trees, Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology, Tabling, Rational Terms, and Coinduction Finally Together!, Craig interpolation with clausal first-order tableaux, Avoiding duplicate proofs with the foothold refinement, A Survey of the Proof-Theoretic Foundations of Logic Programming, Clause trees: A tool for understanding and implementing resolution in automated reasoning, Non-Horn clause logic programming, Computing answers with model elimination, IeanCOP: lean connection-based theorem proving, Abductive reasoning with a large knowledge base for discourse processing, A Prolog assisted search for new simple Lie algebras, Subgoal alternation in model elimination, leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions), Unrestricted resolution versus N-resolution, Improving the time efficiency of proving theorems using a learning mechanism, A semantic backward chaining proof system, Optimizing proof search in model elimination, Efficient model generation through compilation, Linear resolution for consequence finding, A Prolog technology theorem prover: A new exposition and implementation in Prolog, Controlled use of clausal lemmas in connection tableau calculi, Building Theorem Provers, 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, Closures and Modules Within Linear Logic Concurrent Constraint Programming, A novel asynchronous parallelism scheme for first-order logic, Compiling a default reasoning system into Prolog, nanoCoP: A Non-clausal Connection Prover, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Lemma matching for a PTTP-based top-down theorem prover, α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic, Efficient model generation through compilation., From Schütte’s Formal Systems to Modern Automated Deduction, SET-VAR, Logic-based subsumption architecture
Cites Work
- Depth-first iterative-deepening: An optimal admissible tree search
- Non-Horn clause logic programming without contrapositives
- A simplified problem reduction format
- Refutation graphs
- Experimental tests of resolution-based theorem-proving strategies
- Linear resolution with selection function
- Theorem Proving via General Matings
- A Hole in Goal Trees: Some Guidance from Resolution Theory
- Resolution, Refinements, and Search Strategies: A Comparative Study
- An Implementation of the Model Elimination Proof Procedure
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
