Pages that link to "Item:Q1114446"

The following pages link to A Prolog technology theorem prover: Implementation by an extended Prolog compiler (Q1114446):

Displaying 49 items.

• Mark Stickel: his earliest work (Q287332) (← links)
• Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
• Refinements to depth-first iterative-deepening search in automatic theorem proving (Q582116) (← links)
• Compiling a default reasoning system into Prolog (Q750134) (← links)
• Logic-based subsumption architecture (Q814558) (← links)
• Unrestricted resolution versus N-resolution (Q1185013) (← links)
• A semantic backward chaining proof system (Q1193483) (← links)
• Linear resolution for consequence finding (Q1199916) (← links)
• A Prolog technology theorem prover: A new exposition and implementation in Prolog (Q1199932) (← links)
• On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
• SET-VAR (Q1319383) (← links)
• IDNAF Prolog (Q1328781) (← links)
• Problem solving by searching for models with a theorem prover (Q1337680) (← links)
• Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures (Q1340966) (← links)
• Controlled integration of the cut rule into connection tableau calculi (Q1344875) (← links)
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction (Q1344881) (← links)
• The application of automated reasoning to questions in mathematics and logic (Q1354049) (← links)
• A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation (Q1354059) (← links)
• Validation and verification of decision making rules (Q1354851) (← links)
• Clause trees: A tool for understanding and implementing resolution in automated reasoning (Q1402732) (← links)
• Non-Horn clause logic programming (Q1402738) (← links)
• Computing answers with model elimination (Q1402748) (← links)
• IeanCOP: lean connection-based theorem proving (Q1404981) (← links)
• Efficient model generation through compilation. (Q1854374) (← links)
• lean\(T^ AP\): Lean tableau-based deduction (Q1904400) (← links)
• The anatomy of vampire. Implementing bottom-up procedures with code trees (Q1904404) (← links)
• Avoiding duplicate proofs with the foothold refinement (Q1924821) (← links)
• Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
• Improving the time efficiency of proving theorems using a learning mechanism (Q2740950) (← links)
• nanoCoP: A Non-clausal Connection Prover (Q2817929) (← links)
• Tabling, Rational Terms, and Coinduction Finally Together! (Q2931251) (← links)
• History and Prospects for First-Order Automated Deduction (Q3454079) (← links)
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (Q3541708) (← links)
• Subgoal alternation in model elimination (Q4610327) (← links)
• Optimizing proof search in model elimination (Q4647531) (← links)
• Efficient model generation through compilation (Q4647539) (← links)
• Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology (Q4827602) (← links)
• From Schütte’s Formal Systems to Modern Automated Deduction (Q5013905) (← links)
• Prolog Technology Reinforcement Learning Prover (Q5049033) (← links)
• Building Theorem Provers (Q5191110) (← links)
• A novel asynchronous parallelism scheme for first-order logic (Q5210792) (← links)
• Lemma matching for a PTTP-based top-down theorem prover (Q5234698) (← links)
• Closures and Modules Within Linear Logic Concurrent Constraint Programming (Q5458864) (← links)
• α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic (Q5504659) (← links)
• Controlled use of clausal lemmas in connection tableau calculi (Q5927985) (← links)
• Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation (Q5961492) (← links)
• Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles (Q5961493) (← links)
• A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
• A Prolog assisted search for new simple Lie algebras (Q6203472) (← links)