Complexity analysis of propositional resolution with autarky pruning

DOI10.1016/S0166-218X(99)00040-2MaRDI QIDQ1961454zbMATH OpenOpenAlexFDO

Authors Allen Van Gelder

Publication date 13 June 2000

Published in Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0166-218x(99)00040-2

zbMATH Keywords

conjunctive normal formModoc

Mathematics Subject Classification ID

Nonnumerical algorithms (68W05)

Recommendations

• Autarky pruning in propositional model elimination reduces failure redundancy
• A propositional theorem prover to solve planning and other problems
• Parallel cooperative propositional theorem proving
• Lemma and cut strategies for propositional model elimination
• Truth assignments as conditional autarkies

Cites work

• scientific article; zbMATH DE number 515744 (Why is no real title available?)
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Unifying View of Some Linear Herbrand Procedures
• A machine program for theorem-proving
• An extension to linear resolution with selection function
• Autarky pruning in propositional model elimination reduces failure redundancy
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• Controlled integration of the cut rule into connection tableau calculi
• Hard examples for resolution
• Lemma and cut strategies for propositional model elimination
• Linear resolution with selection function
• New methods for 3-SAT decision and worst-case analysis
• Solving satisfiability in less than \(2^ n\) steps

Cited in

(1)

• Minimal sets on propositional formulae. Problems and reductions

This page was built for publication: Complexity analysis of propositional resolution with autarky pruning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1961454)