Optimizing propositional calculus formulas with regard to questions of deducibility

DOI10.1016/0890-5401(89)90021-7zbMath0668.03004OpenAlexW2086598417MaRDI QIDQ1117918

Ulrich Löwen, Hans Kleine Büning

Publication date: 1989

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(89)90021-7

zbMATH Keywords

PROLOGcomputational logicpropositional calculusdecision complexitydeductions of query clausesoptimization of clause forms under resolutionpolynomial time decision problempropositional Horn formulasrestricted optimization problem

Mathematics Subject Classification ID

Related Items (1)

Resolution remains hard under equivalence

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• Complete problems for deterministic polynomial time
• On the complexity of regular resolution and the Davis-Putnam procedure
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Hard examples for resolution
• Unit Refutations and Horn Sets

This page was built for publication: Optimizing propositional calculus formulas with regard to questions of deducibility