Cites work
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- scientific article; zbMATH DE number 3441640 (Why is no real title available?)
- scientific article; zbMATH DE number 3278281 (Why is no real title available?)
- scientific article; zbMATH DE number 3320385 (Why is no real title available?)
- scientific article; zbMATH DE number 3343519 (Why is no real title available?)
- scientific article; zbMATH DE number 3346109 (Why is no real title available?)
- scientific article; zbMATH DE number 3347627 (Why is no real title available?)
- scientific article; zbMATH DE number 3351214 (Why is no real title available?)
- scientific article; zbMATH DE number 3407195 (Why is no real title available?)
- scientific article; zbMATH DE number 3415412 (Why is no real title available?)
- Linear resolution with selection function
- Resolution graphs
- Resolution With Merging
Cited in
(57)- Hierarchical deduction
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A logic for default reasoning
- An extension to linear resolution with selection function
- A simplified problem reduction format
- Reduction rules for resolution-based systems
- Linear resolution for consequence finding
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Refutation graphs
- Recursive query processing: The power of logic
- Theorem proving by chain resolution
- Tractability through symmetries in propositional calculus
- Controlled integration of the cut rule into connection tableau calculi
- On the termination of clause graph resolution
- Generalized disjunctive well-founded semantics for logic programs.
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Stratified resolution
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Weak generalized closed world assumption
- The Q^* algorithm - a search strategy for a deductive question-answering system
- A typed resolution principle for deduction with conditional typing theory
- A logic programming system for nonmonotonic reasoning
- Near-Horn Prolog and the ancestry family of procedures
- Complexity analysis of propositional resolution with autarky pruning
- Milestones from the Pure Lisp Theorem Prover to ACL2
- On the use of stochastic local search techniques to revise first-order logic theories from examples
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Linear resolution with selection function
- A note on linear resolution strategies in consequence-finding
- Mark Stickel: his earliest work
- Efficient description logic reasoning in Prolog: The DLog system
- Abductive inference methods in problems of job planning in complex objects
- Logic and functional programming by retractions
- scientific article; zbMATH DE number 3473353 (Why is no real title available?)
- A note on answer extraction in resolution-based systems
- MRPPS?An interactive refutation proof procedure system for question-answering
- Synthesis of list algorithms by mechanical proving
- On exponential lower bounds for partially ordered resolution
- On linear resolution
- An Interactive Driver for Goal-directed Proof Strategies
- How to produce information about a given entity using automated deduction methods
- Proving with BDDs and control of information
- The complexity of resolution refinements
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- Fuzzy logic programming
- Fifty Years of Prolog and Beyond
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Semantical analysis of the logic of bunched implications
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Prolegomena to logic programming for non-monotonic reasoning
- The relative complexity of analytic tableaux and SL-resolution
- Defining logical systems via algebraic constraints on proofs
- Linearity and regularity with negation normal form
- Termination of floating-point computations
- An epistemic model of logic programming
- A logical characterization of forward and backward chaining in the inverse method
This page was built for publication: Linear resolution with selection function
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2551698)
