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. © Springer-Verlag 2013.

### An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics

#### 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. © Springer-Verlag 2013.
##### Scheda breve Scheda completa Scheda completa (DC)
2013
978-3-642-45220-8
Entailment; Enumeration problems; Horn theory; Modal logics; Satisfiability;
File in questo prodotto:
File
978-3-642-45221-5_1.pdf

solo gestori archivio

Tipologia: Full text (versione editoriale)
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 314.84 kB
Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11392/2330320`