New Results for Horn Cores and Envelopes of Horn Disjunctions

We provide a characterization of Horn cores for formulas in conjunctive normal form (CNF) and, based on it, a novel algorithm for computing Horn cores of disjunctions of Horn CNFs that has appealing properties (e.g., it is polynomial for a bounded disjunction). Furthermore, we show that recognizing the Horn envelope of a disjunction of two Horn CNFs is intractable, and that computing a compact Horn CNF for it (that is irredundant and prime) is not feasible in polynomial total time unless P=NP; this answers an open problem.

• Type: Conference
• Year: 2008
• Where: ECAI
• Authors: Thomas Eiter, Kazuhisa Makino
• Keywords: Artificial Intelligence, Conjunctive Normal Form, ECAI 2008, Horn CNF, Horn Cores