A Prolog technology theorem prover: A new exposition and implementation in Prolog
From MaRDI portal
Recommendations
Cites work
- A logical framework for default reasoning
- A note on linear resolution strategies in consequence-finding
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
- A sequent-style model elimination strategy and a positive refinement
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- An algorithm to compute circumscription
- An examination of the prolog technology theorem-prover
- An Implementation of the Model Elimination Proof Procedure
- Automated deduction by theory resolution
- Depth-first iterative-deepening: An optimal admissible tree search
- scientific article; zbMATH DE number 4180829 (Why is no real title available?)
- scientific article; zbMATH DE number 4164124 (Why is no real title available?)
- scientific article; zbMATH DE number 4164187 (Why is no real title available?)
- scientific article; zbMATH DE number 3978351 (Why is no real title available?)
- scientific article; zbMATH DE number 4049120 (Why is no real title available?)
- scientific article; zbMATH DE number 67457 (Why is no real title available?)
- scientific article; zbMATH DE number 192840 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- Linear resolution with selection function
- Non-Horn clause logic programming without contrapositives
- SETHEO: A high-performance theorem prover
- The Specialization of Programs by Theorem Proving
- The technology chess program
Cited in
(31)- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Prolog technology for default reasoning: proof theory and compilation techniques
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Non-Horn clause logic programming
- IeanCOP: lean connection-based theorem proving
- Practically useful variants of definitional translations to normal form
- Linear and unit-resulting refutations for Horn theories
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Partition-based logical reasoning for first-order and propositional theories
- Mark Stickel: his earliest work
- Semantically-guided goal-sensitive reasoning: model representation
- Logic programming as a basis for lean automated deduction
- Efficient description logic reasoning in Prolog: The DLog system
- scientific article; zbMATH DE number 3986671 (Why is no real title available?)
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- IMPLEMENTING COMPLEX DOMAINS OF APPLICATION IN AN EXTENDED PROLOG SYSTEM
- A new term representation method for prolog
- The theoretical foundations of LPTP (a logic program theorem prover)
- \(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description
- On the practical value of different definitional translations to normal form
- Extensions to logic programming motivated by the construction of a generic theorem prover
- Logistica 2.0: a technology for implementing automatic deduction systems
- Building Theorem Provers
- Lemma matching for a PTTP-based top-down theorem prover
- Mode-Directed Inverse Entailment for Full Clausal Theories
- Prolog Based Description Logic Reasoning
- Fifty Years of Prolog and Beyond
- An examination of the prolog technology theorem-prover
- Compiling a default reasoning system into Prolog
- Logic-based subsumption architecture
This page was built for publication: A Prolog technology theorem prover: A new exposition and implementation in Prolog
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199932)
