Loading...
Please wait, while we are loading the content...
Similar Documents
Disjunctions of Horn Theories and Their Cores Disjunctions of Horn Theories and Their Cores
| Content Provider | Semantic Scholar |
|---|---|
| Author | Ibaraki, Toshihide Makino, Kazuhisa |
| Copyright Year | 1999 |
| Abstract | In this paper, we study issues on disjunctions of propositional Ho rn theories. In particular, we consider deciding whether a disjunction of Horn theories is Hor n, and, if not, computing a Horn core (i.e., a maximal Horn theory included in this disjunction) and Horn envelope (i.e., the minimum Horn theory including the disjunction). The problems are inv stigated for different representations of Horn theories, namely for Horn CNFs and characteristic model s. While the problems are shown to be intractable in general, in the case of bounded disjunction s, we present polynomial time algorithms for testing the Horn property in both representatio ns, and for computing a core in the CNF representation. Even in the case of bounded disjunction, no pol ynomial algorithm exists (unless P=NP) for computing a core in the characteristic model representation . 1Institut und Ludwig Wittgenstein Labor für Informationssystem e, Technische Universität Wien, Treitlstraße 3, A-1040 Wien, Austria. Email: eiter@kr.tuwien.ac.at 2Department of Applied Mathematics and Physics, Graduate School of Informati cs, Kyoto University, Kyoto 606, Japan. Email: ibaraki@kuamp.kyoto-u.ac.jp 3Department of Systems and Human Science, Graduate School of Engineering Science, Osaka University, Toyonaka, Osaka 560, Japan. Email: makino@sys.es.osaka-u.ac.jp Acknowledgements: The authors gratefully acknowledge the partial support of the Scienti fic Grant in Aid by the Ministry of Education, Science and Culture of Japan. Part of this research was conducted while the first author visited Kyoto University in 1995 and 1998, by the supp ort of the Scientific Grant in Aid by the Ministry of Education, Science and Culture of Japan. An abstract containing some results of this paper appears in: Proceedings Nin th An ual Symposium on Algorithms and Computation (ISAAC ’98), Taejon, Korea, K.-Y. Chwa and O. H. Ibarra, eds, LNCS 1533, pages 49–58. Springer, 1998. A previous version of this paper contain ing a subset of the results is available as RUTCOR Research Report RRR 24-98, September 1998. Copyright c 1999 by the authors 2 INFSYS RR 1843-99-02 |
| File Format | PDF HTM / HTML |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
