Unrestricted vs restricted cut in a tableau method for Boolean circuits

DOI10.1007/S10472-005-7034-1MaRDI QIDQ812394zbMATH OpenOpenAlexFDO

Authors Matti Järvisalo, Tommi Junttila, Ilkka Niemelä

Publication date 23 January 2006

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-005-7034-1

zbMATH Keywords

Boolean circuitsproof complexitysatisfiabilitycut ruleDPLLtableau method

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Complexity of proofs (03F20)

Recommendations

• scientific article; zbMATH DE number 1696820
• scientific article; zbMATH DE number 1552525
• scientific article; zbMATH DE number 1189106
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• The complexity of analytic tableaux

Cites work

• scientific article; zbMATH DE number 1670796 (Why is no real title available?)
• scientific article; zbMATH DE number 1189106 (Why is no real title available?)
• scientific article; zbMATH DE number 1324671 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 1113992 (Why is no real title available?)
• scientific article; zbMATH DE number 1179974 (Why is no real title available?)
• scientific article; zbMATH DE number 1538056 (Why is no real title available?)
• scientific article; zbMATH DE number 1798189 (Why is no real title available?)
• scientific article; zbMATH DE number 2090309 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A deterministic \((2-2/(k+1))^{n}\) algorithm for \(k\)-SAT based on local search.
• A machine program for theorem-proving
• A structure-preserving clause form translation
• Bounded model checking using satisfiability solving
• Principles and Practice of Constraint Programming – CP 2004
• The Taming of the Cut. Classical Refutations with Analytic Cut
• The efficiency of resolution and Davis-Putnam procedures
• The intractability of resolution

Cited in

(7)

• Solving satisfiability problems with preferences
• Limitations of restricted branching in clause learning
• On exponential lower bounds for partially ordered resolution
• A general framework for preferences in answer set programming
• Limitations of Restricted Branching in Clause Learning
• Implementing preferences with asprin
• Algorithms for Solving Satisfiability Problems with Qualitative Preferences

Describes a project that uses

Uses Software

• Chaff
• Walksat

This page was built for publication: Unrestricted vs restricted cut in a tableau method for Boolean circuits

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