Linear resolution with selection function

DOI10.1016/0004-3702(71)90012-9zbMath0234.68037OpenAlexW4229861117MaRDI QIDQ2551698

Donald Kuehner, Robert Kowalski

Publication date: 1971

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(71)90012-9

Mathematics Subject Classification ID

Related Items (53)

On the use of stochastic local search techniques to revise first-order logic theories from examples ⋮ Tractability through symmetries in propositional calculus ⋮ Mark Stickel: his earliest work ⋮ Controlled integration of the cut rule into connection tableau calculi ⋮ On the termination of clause graph resolution ⋮ A logic programming system for nonmonotonic reasoning ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Hierarchical deduction ⋮ Generalized disjunctive well-founded semantics for logic programs. ⋮ Termination of floating-point computations ⋮ A Prolog technology theorem prover: Implementation by an extended Prolog compiler ⋮ Abductive inference methods in problems of job planning in complex objects ⋮ Near-Horn Prolog and the ancestry family of procedures ⋮ Fifty Years of Prolog and Beyond ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ A logic for default reasoning ⋮ Semantical analysis of the logic of bunched implications ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ Stratified resolution ⋮ An extension to linear resolution with selection function ⋮ An epistemic model of logic programming ⋮ Complexity analysis of propositional resolution with autarky pruning ⋮ A simplified problem reduction format ⋮ A logical characterization of forward and backward chaining in the inverse method ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Synthesis of list algorithms by mechanical proving ⋮ Reduction rules for resolution-based systems ⋮ Logic and functional programming by retractions ⋮ Linear resolution for consequence finding ⋮ A Prolog technology theorem prover: A new exposition and implementation in Prolog ⋮ The relative complexity of analytic tableaux and SL-resolution ⋮ An Interactive Driver for Goal-directed Proof Strategies ⋮ How to Produce Information About a Given Entity Using Automated Deduction Methods ⋮ Linearity and regularity with negation normal form ⋮ Fuzzy logic programming ⋮ Refutation graphs ⋮ The complexity of resolution refinements ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Proving with BDDs and control of information ⋮ Recursive query processing: The power of logic ⋮ A note on answer extraction in resolution-based systems ⋮ Efficient description logic reasoning in Prolog: The DLog system ⋮ Theorem proving by chain resolution ⋮ Weak generalized closed world assumption ⋮ Linear resolution with selection function ⋮ A note on linear resolution strategies in consequence-finding ⋮ A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs ⋮ The \(Q^*\) algorithm - a search strategy for a deductive question-answering system ⋮ Unnamed Item ⋮ A typed resolution principle for deduction with conditional typing theory ⋮ On Exponential Lower Bounds for Partially Ordered Resolution ⋮ On Linear Resolution ⋮ MRPPS?An interactive refutation proof procedure system for question-answering

Cites Work

• Resolution graphs
• Linear resolution with selection function
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Resolution With Merging
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Linear resolution with selection function