Polynomial-time inference of all valid implications for Horn and related formulae

E. Boros, Y. Crama, P. L. Hammer

Research output: Contribution to journalArticlepeer-review

79 Scopus citations


This paper investigates the complexity of a general inference problem: given a propositional formula in conjunctive normal form, find all prime implications of the formula. Here, a prime implication means a minimal clause whose validity is implied by the validity of the formula. We show that, under some reasonable assumptions, this problem can be solved in time polynomially bounded in the size of the input and in the number of prime implications. In the case of Horn formulae, the result specializes to yield an algorithm whose complexity grows only linearly with the number of prime implications. The result also applies to a class of formulae generalizing both Horn and quadratic formulae.

Original languageEnglish (US)
Pages (from-to)21-32
Number of pages12
JournalAnnals of Mathematics and Artificial Intelligence
Issue number1-4
StatePublished - Sep 1990

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Applied Mathematics


  • Horn formulae
  • Propositional logic
  • complexity
  • inference
  • resolution


Dive into the research topics of 'Polynomial-time inference of all valid implications for Horn and related formulae'. Together they form a unique fingerprint.

Cite this