scientific article; zbMATH DE number 1470716
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)
- 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
- A decomposition method for CNF minimality proofs
- On the query complexity of selecting minimal sets for monotone predicates
- A CNF Class Generalizing Exact Linear Formulas
- On the computational consequences of independence in propositional logic
- Satisfiability of mixed Horn formulas
- IASCAR: incremental answer set counting by anytime refinement
- 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
- Quantifier reordering for QBF
- Exploiting Database Management Systems and Treewidth for Counting
- Ground Interpolation for Combined Theories
- Propositional SAT solving
- On conversions from CNF to ANF
- Minimal sets on propositional formulae. Problems and reductions
- Solving projected model counting by utilizing treewidth and its limits
- Failed literal detection for QBF
- Directed hypergraphs and Horn minimization
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- Backdoor sets of quantified Boolean formulas
- The treewidth of proofs
- Total space in resolution
- scientific article; zbMATH DE number 782033 (Why is no real title available?)
- Extension and equivalence problems for clause minimal formulae
- Boolean functions with long prime implicants
- Generalizations of matched CNF formulas
- Models and quantifier elimination for quantified Horn formulas
- Introduction to Mathematics of Satisfiability
- Subsumption-linear Q-resolution for QBF theorem proving
- On the benefits of knowledge compilation for feature-model analyses
- Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all?
- scientific article; zbMATH DE number 1705165 (Why is no real title available?)
- Tight double exponential lower bounds
- Boolean functions as models for quantified Boolean formulas
- Combinatorial Problems for Horn Clauses
- Small resolution proofs for QBF using dependency treewidth
- A logic-based approach to polymer sequence analysis
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
- Using decomposition-parameters for QBF: mind the prefix!
- Backdoors into two occurrences
- Learning definite Horn formulas from closure queries
- Constraint acquisition
- Solving peptide sequencing as satisfiability
- The complexity of problems for quantified constraints
- Theory revision with queries: Horn, read-once, and parity formulas
- Inductive definitions in logic versus programs of real-time cellular automata
- Boolean Constraint Satisfaction Problems: When Does Post’s Lattice Help?
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)
