scientific article; zbMATH DE number 1470716
algorithmscomplexity analysiscomputation problemscutting plane algorithmsdata structuresessentially quantified Boolean termsextension of propositional logicFrege systemsHorn logiclength of resolution proofslinear inequation systemnormal formsNP-completenesspropositional logicresolution calculussatisfiability checking algorithmssatisfiability problem for clausessequent systemstableauxtransformation algorithms
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25) Analysis of algorithms (68W40)
[For a review of the German original (Teubner, Stuttgart, 1994) see Zbl 0809.03003.] This book contains a treatment of propositional logic, both from a classical mathematical standpoint, as well as from a modern computer-oriented standpoint, e.g. treating data structures for the representation of formulas and clauses, implementation details for several calculi and deduction algorithms, as well as worst-case and average-case complexity estimations. In this respect, the topics treated in this book and the style of presentation, as well as the computer science viewpoint to logic, is quite unique and refreshing. The first chapter deals with notation and basic results. Then, in the second chapter, data structures for the representation of clauses and normal forms are discussed, including binary decision diagrams. The satisfiability problem of propositional logic (which is NP-complete) and various algorithms and deduction systems for solving it, like the Davis-Putnam algorithm, are discussed in detail in Chapter 3. A large part of Chapter 3 is devoted to the complexity of a variety of satisfiability problems, or problems derived from satisfiability problems. Most of them turn out to be NP-complete, but some are complete for other classes, like PSPACE or DP. Another aspect is the evolution of random satisfiability instances. Random formulas with few clauses tend to be satisfiable, then, starting at a certain threshold, random formulas with many clauses tend to be unsatisfiable. Resolution as a special system with a variety of computer science applications, its refinements and evaluation strategies are the themes of Chapter 4. The special case of Horn formulas together with deduction systems tailored for Horn logic is treated in the fifth chapter. Chapter 6 discusses all the other known calculi -- specialized to the case of propositional logic: Frege systems, cutting planes, tableau, segment calculus, and Gentzen systems. The relative strengths of these systems are compared. In Chapter 7, propositional formulas are equipped with quantifiers, but quantifiers that range only over Boolean values. These QBF formulas can be understood as some kind of intermediate step between propositional logic and predicate logic. Again, similar variations and algorithms as in the propositional case are presented for QBF.
- scientific article; zbMATH DE number 702472
- scientific article; zbMATH DE number 4008367
- The propositional logic induced by means of basic algebras
- scientific article; zbMATH DE number 4039849
- scientific article; zbMATH DE number 4031629
- scientific article; zbMATH DE number 3259885
- scientific article; zbMATH DE number 6001202
- scientific article; zbMATH DE number 4079387
- Backdoor sets of quantified Boolean formulas
- Optimizing propositional calculus formulas with regard to questions of deducibility
- Homomorphisms of conjunctive normal forms.
- Minimal sets on propositional formulae. Problems and reductions
- On exact selection of minimally unsatisfiable subformulae
- Generalizations of matched CNF formulas
- Extension and equivalence problems for clause minimal formulae
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
- The complexity of problems for quantified constraints
- The treewidth of proofs
- Using decomposition-parameters for QBF: mind the prefix!
- On conversions from CNF to ANF
- Directed hypergraphs and Horn minimization
- Boolean functions with long prime implicants
- On the computational consequences of independence in propositional logic
- On the query complexity of selecting minimal sets for monotone predicates
- Boolean functions as models for quantified Boolean formulas
- Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all?
- Solving projected model counting by utilizing treewidth and its limits
- Propositional reasoning
- Total space in resolution
- Quantifier reordering for QBF
- Failed literal detection for QBF
- Generalized conflict-clause strengthening for satisfiability solvers
- Propositional SAT solving
- Small resolution proofs for QBF using dependency treewidth
- Introduction to Mathematics of Satisfiability
- A CNF Class Generalizing Exact Linear Formulas
- Combinatorial Problems for Horn Clauses
- A decomposition method for CNF minimality proofs
- Boolean functions with a simple certificate for CNF complexity
- Construction and learnability of canonical Horn formulas
- Reasoning about visibility
- scientific article; zbMATH DE number 702472 (Why is no real title available?)
- scientific article; zbMATH DE number 1380573 (Why is no real title available?)
- scientific article; zbMATH DE number 782033 (Why is no real title available?)
- Backdoors into two occurrences
- Learning definite Horn formulas from closure queries
- Constraint acquisition
- Ground Interpolation for Combined Theories
- Boolean Constraint Satisfaction Problems: When Does Post’s Lattice Help?
- Exploiting Database Management Systems and Treewidth for Counting
- Inductive definitions in logic versus programs of real-time cellular automata
- Subsumption-linear Q-resolution for QBF theorem proving
- Logic-based ontology comparison and module extraction, with an application to DL-Lite
- A logic-based approach to polymer sequence analysis
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- On the benefits of knowledge compilation for feature-model analyses
- Tight double exponential lower bounds
- IASCAR: incremental answer set counting by anytime refinement
- Small unsatisfiable k-CNFs with bounded literal occurrence
- The relative strength of \#SAT proof systems
- Refinement-based enumeration of QBF solutions
- Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
- Producing and verifying extremely large propositional refutations
- Counting QBF solutions at level two
- The complexity of variable minimal formulas
- Inferring RPO symbol orderings
- The relative strength of \#SAT proof systems
- Body-decoupled grounding via reduction: a novel approach on the \textsc{Asp} bottleneck
- Generating theorems by generating proof structures
- Theory revision with queries: Horn, read-once, and parity formulas
- Solving peptide sequencing as satisfiability
- Models and quantifier elimination for quantified Horn formulas
- Exclusive and essential sets of implicates of Boolean functions
- A new 3-CNF transformation by parallel-serial graphs
- Satisfiability of mixed Horn formulas
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4488342)
