Abstract
The fragment of propositional logic known as Horn theories plays a central role in automated reasoning. The problem of enumerating the maximal models of a Horn theory (MaxMod) has been proved to be computationally hard, unless P = NP. To the best of our knowledge, the only algorithm available for it is the one based on a brute-force approach. In this paper, we provide an algorithm for the problem of enumerating the maximal subsets of facts that do not entail a distinguished atomic proposition in a definite Horn theory (MaxNoEntail). We show that MaxMod is polynomially reducible to MaxNoEntail (and vice versa), making it possible to solve also the former problem using the proposed algorithm. Addressing MaxMod via MaxNoEntail opens, inter alia, the possibility of benefiting from the monotonicity of the notion of entailment. (The notion of model does not enjoy such a property.) We also discuss an application of MaxNoEntail to expressiveness issues for modal logics, which reveals the effectiveness of the proposed algorithm.
The authors acknowledge the support from the Spanish fellowship program ‘Ramon y Cajal’ RYC-2011-07821 and the Spanish MEC project TIN2009-14372-C03-01 (G. Sciavicco), the project Processes and Modal Logics (project nr. 100048021) of the Icelandic Research Fund (L. Aceto, D. Della Monica, and A. Ingólfsdóttir), the project Decidability and Expressiveness for Interval Temporal Logics (project nr. 130802-051) of the Icelandic Research Fund (D. Della Monica), and the Italian GNCS project Extended Game Logics (A. Montanari).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cook, S.: The complexity of theorem proving procedures. In: Proc. of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151–158 (1971)
Chang, C., Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving, 1st edn. Academic Press, Inc. (1997)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer (1987)
Kautz, H., Mcallester, D., Selman, B.: Encoding plans in propositional logic. In: Proc. of the 5th KR, pp. 374–384 (1996)
Riesbeck, C., Schank, R.: Inside Case-based Reasoning. Artificial intelligence series. Lawrence Erlbaum (1989)
Brachman, R., Levesque, H.: Knowledge Representation and Reasoning. Morgan Kaufmann Publishers Inc. (2004)
Brusoni, V., Console, L., Terenziani, P., Dupré, D.T.: Characterizing temporal abductive diagnosis. In: Proc. of the 6th DX, pp. 34–40 (1995)
Cadoli, M.: The complexity of model checking for circumscriptive formulae. Information Processing Letters 44, 113–118 (1992)
Kavvadias, D.J., Sideri, M., Stavropoulos, E.: Generating all maximal models of a Boolean expression. Inf. Process. Lett. 74(3-4), 157–162 (2000)
Knuth, D.: The Art of Computer Programming: Combinatorial Algorithms, Part 1, 1st edn., vol. 4A. Addison-Wesley Professional (2011)
Schmidt, J.: Enumeration: Algorithms and complexity. Unpublished (2009)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2002)
Aceto, L., Della Monica, D., Ingólfsdóttir, A., Montanari, A., Sciavicco, G.: A complete classification of the expressiveness of interval logics of Allen’s relations over dense linear orders. In: Proc. of the 20th TIME (2013)
Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Expressiveness of the interval logics of Allen’s relations on the class of all linear orders: Complete classification. In: Proc. of the 22nd IJCAI, pp. 845–850 (2011)
Balbiani, P., Goranko, V., Sciavicco, G.: Two-sorted point-interval temporal logics. Electr. Notes Theor. Comput. Sci. 278, 31–45 (2011)
Halpern, J., Shoham, Y.: A propositional modal logic of time intervals. Journal of the ACM 38(4), 935–962 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Della Monica, D., Ingólfsdóttir, A., Montanari, A., Sciavicco, G. (2013). An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)