scientific article; zbMATH DE number 1470716

zbMath0957.03001MaRDI QIDQ4488342

Hans Kleine Büning, Theodor Lettmann

Publication date: 5 July 2000

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

algorithmsnormal formstableauxpropositional logicNP-completenessdata structurescomplexity analysisresolution calculusHorn logiccutting plane algorithmsFrege systemssequent systemscomputation problemstransformation algorithmsessentially quantified Boolean termsextension of propositional logiclength of resolution proofssatisfiability checking algorithmssatisfiability problem for clauseslinear inequation system

Mathematics Subject Classification ID

Related Items (48)

Quantifier reordering for QBF ⋮ Propositional SAT Solving ⋮ Boolean functions as models for quantified Boolean formulas ⋮ Directed hypergraphs and Horn minimization ⋮ Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all? ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ Small Resolution Proofs for QBF using Dependency Treewidth ⋮ A decomposition method for CNF minimality proofs ⋮ Exploiting Database Management Systems and Treewidth for Counting ⋮ A CNF Class Generalizing Exact Linear Formulas ⋮ Logic-based ontology comparison and module extraction, with an application to DL-Lite ⋮ Solving projected model counting by utilizing treewidth and its limits ⋮ Boolean functions with a simple certificate for CNF complexity ⋮ Inductive definitions in logic versus programs of real-time cellular automata ⋮ Construction and learnability of canonical Horn formulas ⋮ Reasoning about visibility ⋮ Subsumption-linear Q-resolution for QBF theorem proving ⋮ Homomorphisms of conjunctive normal forms. ⋮ The complexity of problems for quantified constraints ⋮ Boolean functions with long prime implicants ⋮ A logic-based approach to polymer sequence analysis ⋮ Solving peptide sequencing as satisfiability ⋮ Models and quantifier elimination for quantified Horn formulas ⋮ Failed Literal Detection for QBF ⋮ Generalized Conflict-Clause Strengthening for Satisfiability Solvers ⋮ Learning definite Horn formulas from closure queries ⋮ Constraint acquisition ⋮ Producing and verifying extremely large propositional refutations ⋮ Exclusive and essential sets of implicates of Boolean functions ⋮ The treewidth of proofs ⋮ A new 3-CNF transformation by parallel-serial graphs ⋮ The complexity of variable minimal formulas ⋮ On exact selection of minimally unsatisfiable subformulae ⋮ Generalizations of matched CNF formulas ⋮ Extension and equivalence problems for clause minimal formulae ⋮ Ground Interpolation for Combined Theories ⋮ On the computational consequences of independence in propositional logic ⋮ Recognizing read-once functions from depth-three formulas ⋮ Satisfiability of mixed Horn formulas ⋮ Using decomposition-parameters for QBF: mind the prefix! ⋮ On conversions from CNF to ANF ⋮ Total Space in Resolution ⋮ Combinatorial Problems for Horn Clauses ⋮ Backdoor sets of quantified Boolean formulas ⋮ Boolean Constraint Satisfaction Problems: When Does Post’s Lattice Help? ⋮ Backdoors into Two Occurrences ⋮ On the query complexity of selecting minimal sets for monotone predicates ⋮ Theory revision with queries: Horn, read-once, and parity formulas

This page was built for publication: