A Prolog technology theorem prover: Implementation by an extended Prolog compiler
From MaRDI portal
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
- scientific article; zbMATH DE number 1424017
- Proof-theoretic and higher-order extensions of logic programming
Cites work
- scientific article; zbMATH DE number 3986666 (Why is no real title available?)
- scientific article; zbMATH DE number 3657150 (Why is no real title available?)
- scientific article; zbMATH DE number 3774914 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 3395362 (Why is no real title available?)
- scientific article; zbMATH DE number 3407199 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- A Hole in Goal Trees: Some Guidance from Resolution Theory
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A simplified problem reduction format
- An Implementation of the Model Elimination Proof Procedure
- Depth-first iterative-deepening: An optimal admissible tree search
- Experimental tests of resolution-based theorem-proving strategies
- Linear resolution with selection function
- Non-Horn clause logic programming without contrapositives
- Refutation graphs
- Resolution, Refinements, and Search Strategies: A Comparative Study
- Theorem Proving via General Matings
Cited in
(64)- Efficient model generation through compilation.
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Building Theorem Provers
- 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
- Lemma matching for a PTTP-based top-down theorem prover
- A Mizar mode for HOL
- Unrestricted resolution versus N-resolution
- 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
- Improving the time efficiency of proving theorems using a learning mechanism
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- From Schütte’s Formal Systems to Modern Automated Deduction
- Avoiding duplicate proofs with the foothold refinement
- Mark Stickel: his earliest work
- Semantically-guided goal-sensitive reasoning: model representation
- Linear resolution for consequence finding
- An examination of the prolog technology theorem-prover
- Closures and Modules Within Linear Logic Concurrent Constraint Programming
- Non-Horn clause logic programming
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- 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
- SET-VAR
- 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
- 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
- IeanCOP: lean connection-based theorem proving
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- IDNAF Prolog
- scientific article; zbMATH DE number 1614712 (Why is no real title available?)
- scientific article; zbMATH DE number 1552514 (Why is no real title available?)
- Craig interpolation with clausal first-order tableaux
- Problem solving by searching for models with a theorem prover
- Abductive reasoning with a large knowledge base for discourse processing
- A Prolog assisted search for new simple Lie algebras
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Partheo: A high-performance parallel theorem prover
- A novel asynchronous parallelism scheme for first-order logic
- A semantic backward chaining proof system
- Subgoal alternation in model elimination
- The application of automated reasoning to questions in mathematics and logic
- Efficient model generation through compilation
- Investigations into proof structures
- A complete semantic back chaining proof system
- 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
- Lemmas: generation, selection, application
- Range-restricted and Horn interpolation through clausal tableaux
- lean\(T^ AP\): Lean tableau-based deduction
- Logic-based subsumption architecture
- scientific article; zbMATH DE number 3986671 (Why is no real title available?)
- Prolog Technology Reinforcement Learning Prover
- nanoCoP: a non-clausal connection prover
- scientific article; zbMATH DE number 3965464 (Why is no real title available?)
- A Survey of the Proof-Theoretic Foundations of Logic Programming
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)
