Autarky pruning in propositional model elimination reduces failure redundancy

DOI10.1023/A:1006143621319MaRDI QIDQ1808886zbMATH OpenOpenAlexFDO

Authors Allen Van Gelder

Publication date 25 November 1999

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1006143621319

zbMATH Keywords

model elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Complexity analysis of propositional resolution with autarky pruning
• Lemma and cut strategies for propositional model elimination
• A propositional theorem prover to solve planning and other problems
• Parallel cooperative propositional theorem proving
• Persistent and quasi-persistent lemmas in propositional model elimination

Cited in

(10)

• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Persistent and quasi-persistent lemmas in propositional model elimination
• Minimal sets on propositional formulae. Problems and reductions
• Investigations on autark assignments
• Complexity analysis of propositional resolution with autarky pruning
• A propositional theorem prover to solve planning and other problems
• Another look at graph coloring via propositional satisfiability
• A Decision-Making Procedure for Resolution-Based SAT-Solvers
• An overview of parallel SAT solving
• Subsumption-linear Q-resolution for QBF theorem proving

Describes a project that uses

Uses Software

• Walksat
• SATO

This page was built for publication: Autarky pruning in propositional model elimination reduces failure redundancy

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