scientific article; zbMATH DE number 1470716
zbMATH Open0957.03001MaRDI QIDQ4488342FDOQ4488342
Authors: Hans Kleine Büning, Theodor Lettmann 
Publication date: 5 July 2000
Title of this publication is not available (Why is that?)
Recommendations
- 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
algorithmsdata structuresnormal formsNP-completenesscomplexity analysistableauxpropositional logicHorn logicresolution calculuscutting plane algorithmsFrege systemssequent systemscomputation problemstransformation algorithmsessentially quantified Boolean termsextension of propositional logiclength of resolution proofssatisfiability checking algorithmssatisfiability problem for clauseslinear inequation system
Analysis of algorithms and problem complexity (68Q25) Analysis of algorithms (68W40) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Complexity of proofs (03F20) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Cited In (56)
- IASCAR: incremental answer set counting by anytime refinement
- 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
- A decomposition method for CNF minimality proofs
- A CNF Class Generalizing Exact Linear Formulas
- On the query complexity of selecting minimal sets for monotone predicates
- On the computational consequences of independence in propositional logic
- Satisfiability of mixed Horn formulas
- Generalized conflict-clause strengthening for satisfiability solvers
- Logic-based ontology comparison and module extraction, with an application to DL-Lite
- Boolean functions with a simple certificate for CNF complexity
- Homomorphisms of conjunctive normal forms.
- Producing and verifying extremely large propositional refutations
- Exclusive and essential sets of implicates of Boolean functions
- Construction and learnability of canonical Horn formulas
- Reasoning about visibility
- A new 3-CNF transformation by parallel-serial graphs
- The complexity of variable minimal formulas
- On exact selection of minimally unsatisfiable subformulae
- Optimizing propositional calculus formulas with regard to questions of deducibility
- Exploiting Database Management Systems and Treewidth for Counting
- Ground Interpolation for Combined Theories
- Quantifier reordering for QBF
- Propositional SAT solving
- On conversions from CNF to ANF
- Solving projected model counting by utilizing treewidth and its limits
- Minimal sets on propositional formulae. Problems and reductions
- Failed literal detection for QBF
- Directed hypergraphs and Horn minimization
- Backdoor sets of quantified Boolean formulas
- Title not available (Why is that?)
- The treewidth of proofs
- Total space in resolution
- Extension and equivalence problems for clause minimal formulae
- Boolean functions with long prime implicants
- Generalizations of matched CNF formulas
- Subsumption-linear Q-resolution for QBF theorem proving
- Introduction to Mathematics of Satisfiability
- Models and quantifier elimination for quantified Horn formulas
- Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all?
- Title not available (Why is that?)
- Boolean functions as models for quantified Boolean formulas
- Combinatorial Problems for Horn Clauses
- Small resolution proofs for QBF using dependency treewidth
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
- A logic-based approach to polymer sequence analysis
- Backdoors into two occurrences
- Using decomposition-parameters for QBF: mind the prefix!
- Solving peptide sequencing as satisfiability
- Learning definite Horn formulas from closure queries
- Constraint acquisition
- The complexity of problems for quantified constraints
- Inductive definitions in logic versus programs of real-time cellular automata
- Boolean Constraint Satisfaction Problems: When Does Post’s Lattice Help?
- Theory revision with queries: Horn, read-once, and parity 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)
