Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics
verfasst von : Luca Aceto, Dario Della Monica, Anna Ingólfsdóttir, Angelo Montanari, Guido Sciavicco
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.