scientific article; zbMATH DE number 702472

zbMath0809.03003MaRDI QIDQ4315881

Theodor Lettmann, Hans Kleine Büning

Publication date: 12 December 1994

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

zbMATH Keywords

algorithmsnormal formstableauxpropositional logicdata structuresHorn clausescomplexity analysisresolution calculusHorn logiccutting plane algorithmsFrege systemssequent systemscomputation problemstransformation algorithmsessentially quantified Boolean termsextension of propositional logiclength of resolution proofslinear inequation systemssatisfiability checking algorithmssatisfiability problem for clauses

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) 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) Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items

Improving a fixed parameter tractability time bound for the shadow problem ⋮ On the complexity of resolution with bounded conjunctions ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Short proofs for some symmetric quantified Boolean formulas ⋮ Space bounds for resolution

This page was built for publication: