Parametrized logic programs are very expressive logic programs that generalize normal logic programs under the stable model semantics, by allowing complex formulas of a parameter logic to appear in the body and head of rules. In this paper we explore the use of description logics as parameter logics, and show the expressivity of this framework for combining rules and ontologies.
Parametrized logic programming [Gonc¸alves and Alferes, 2010] was introduced as an extension of answer set programming [Gelfond and Lifschitz, 1988] with the motivation of providing a meaning to theories combining both logic programming connectives with other logical connectives, and allowing complex formulas using these connectives to appear in the head and body of a rule. The main idea is to fix a monotonic logic L, called the parameter logic, and build up logic programs using formulas of L instead of just atoms. The obtained parametrized logic programs have, therefore, the same structure of normal logic programs, being the only difference the fact that atomic symbols are replaced by formulas of L.
When applying this framework, the choice of the parameter logic depends on the domain of the problem to be modeled. As examples, [Gonc¸alves and Alferes, 2010] shows how to obtain the answer-set semantics of logic programs with explicit negation, a paraconsistent version of it, and also the semantics of MKNF hybrid knowledge bases [Motik and Rosati, 2010], using an appropriate choice of the parameter logic. In [Gonc¸alves and Alferes, 2012] deontic logic programs are introduced using standard deontic logic [von Wright, 1951] as the parameter logic. Moreover, in [Gonc¸alves and Alferes, 2013] the decidability and implementation of parametrized logic was discussed.
Parametrized logic programming can thus be seen as a framework which allows to add non-monotonic rule based reasoning on top of an existing (monotonic) language. This view is quite interesting, in particular in those cases where we already have a monotonic logic to model a problem, but we are still lacking some conditional or non-monotonic reasoning. In these situations, parametrized logic programming offers a modular framework for adding such conditional and non-monotonic reasoning, without having to give up of the monotonic logic at hand.
In recent years, there has been a considerable amount of effort devoted to combining Description Logics (DLs) with logic programming non-monotonic rules – see, e.g., related work in [Eiter et al., 2008; Motik and Rosati, 2010].
In this paper we explore precisely the use of description logics as parameter logics, and show the expressivity of the resulting framework for combining rules and ontologies.
Parametrized logic programs are very expressive logic programs that generalize normal logic programs under the stable model semantics, by allowing complex formulas of a parameter logic to appear in the body and head of rules. In this section we introduce the syntax and semantics of normal parametrized logic programs [Gonc¸alves and Alferes, 2010].
The syntax of a normal parametrized logic program has the same structure of that of a normal logic program. The only difference is that the atomic symbols of a normal parametrized logic program are replaced by formulas of a parameter logic, which is restricted to be a monotonic logic. Let us start by introducing the necessary concepts related with the notion of (monotonic) logic.
Definition 1 A (monotonic) logic is a pair L = hL; `Li where L is a set of formulas and `L is a Tarskian consequence relation [W o´jcicki, 1988] over L, i.e., satisfying the following conditions, for every T [ [ f'g L,
Cut: if T `L ' for all ' 2 , and
`L then then T `L
; `L '.
When clear from the context we write ` instead of `L. Let T h(L) be the set of logical theories of L, i.e. the set of subsets of L closed under the relation `L. One fundamental characteristic of the above definition of monotonic logic is that it has as a consequence that, for every (monotonic) logic L, the tuple hT h(L); i is a complete lattice with smallest element the set T heo = ;` of theorems of L and the greatest element the set L of all formulas of L. Given a subset A of L we denote by A`L the smallest logical theory of L that contains A. A`L is also called the logical theory generated by A in L.
In what follows we consider fixed a (monotonic) logic L = hL; `Li and call it the parameter logic. The formulas of L are dubbed (parametrized) atoms and a (parametrized) literal is either a parametrized atom ' or its negation not ', where as usual not denotes negation as failure. We dub default literal those of the form not '.
Definition 2 A normal L parametrized logic program is a set of rules ' 1; : : : ; n; not 1; : : : ; not m (1) where '; 1; : : : ; n; 1; : : : ; m 2 L.
A definite L parametrized logic program is a set of rules without negations as failure, i.e. of the form ' 1; : : : ; n where '; 1; : : : ; n 2 L.
As usual, the symbol represents rule implication, the symbol “,” represents conjunction and the symbol not represents default negation. A rule as (1) has the usual reading that ' should hold whenever 1; : : : ; n hold and 1; : : : ; m are not known to hold. If n = 0 and m = 0 then we just write ' .
Given a rule r of the form (1), we define head(r) = ', body+(r) = f 1; : : : ; ng, body (r) = f 1; : : : ; mg and body(r) = body+(r) [ body (r). Given a parametrized logic program P we define f orm(P) to be the set of all formulas of the parameter language L appearing in P, i.e., f orm(P) = Sr2P (fhead(r)g [ body(r)). We also define the set head(P) = fhead(r) : r 2 Pg.
Given this general language of parametrized logic programs, we define its stable model semantics, as generalization of the stable model semantics [Gelfond and Lifschitz, 1988] of normal logic programs.
In the traditional approach an interpretation is just a set of atoms. In a parametrized logic program, since we substitute atoms by formulas of a parameter logic, the first idea is to take sets of formulas of the parameter logic as interpretations. The problem is that, contrary to the case of atoms, the parametrized atoms are not independent of each other. This interdependence is governed by the consequence relation of the parameter logic. For example, if we take classical propositional logic (CPL) as the parameter logic, we have that if the parametrized atom p ^ q is true then so are the parametrized atoms p and q. If we take, for example, standard deontic logic SDL [von Wright, 1951] as parameter, we have that, since O(p _ q); O(:p) `SDL O(q), any SDL logical theory containing both O(p _ q) and O(:p) also contains O(q).
To account for this interdependence, we use logical theories (sets of formulas closed under the consequence of the logic) as the generalization of interpretations, thus capturing the above mentioned interdependence.
Definition 3 A (parametrized) interpretation is a logical theory of L.
Definition 4 An interpretation T satisfies a rule '
1; : : : ; n; not 1; : : : ; not m if ' 2 T whenever i 2 T for every i 2 f1; : : : ; ng and j 2= T for every j 2 f1; : : : ; mg.
An interpretation is a model of logic program P if it satisfies every rule of P. We denote by M odL(P ) the set of models of P .
The ordering over interpretations is the usual one: If T1 and T2 are two interpretations then we say that T1 T2 if T1 T2. Moreover, given such ordering, minimal and least interpretations may be defined in the usual way.
As in the case of non parametrized programs, we start by assigning semantics to definite parametrized programs. Recall that the stable model of a definite logic program is its least model. In order to generalize this definition to the parametrized case we need to establish that the least parametrized model exists for every definite L parametrized logic program.
Theorem 1 Every definite L parametrized logic program has a least model.
We denote by SPL the least model of a definite program P .
It is important to note that Theorem 1 holds for every choice of the parameter logic L.
The stable model semantics of a normal L parametrized logic program is defined using a Gelfond-Lifschitz like operator.
Definition 5 Let P be a normal L parametrized logic program and T an interpretation. The GL-transformation of P modulo T is the program PT obtained from P by performing the following operations: remove from P all rules which contain a literal not ' such that T `L '; remove from the remaining rules all default literals. Since PT is a definite L parametrized program, it has an unique least model J . We define (T ) = J .
Stable models of a parametrized logic program are then defined as fixed points of this operator.
Definition 6 An interpretation T of an L parametrized logic program P is a stable model of P iff (T ) = T . A formula ' is true under the stable model semantics, denoted by P SMS ' iff it belongs to all stable models of P.
An important feature of parametrized logic programming is that its stable model semantics is independent of the semantics of the parameter logic, since the central concept is the consequence relation of the parameter logic.
Let us now show an example of how parametrized logic programs can be used to combine a monotonic formalism with a non-monotonic one. We choose three different logics over the same propositional language.
consider a full propositional language L built over a set P of propositional symbols using the usual connectives (:; _; ^; )). Many consequence relations can be defined over this language. We present three interesting examples: classical logic, Belnap’s paraconsistent logic and intuitionistic logic. Consider the following programs: This means that p; :p; q; :q 2= SPC1P L. We also have that SPC2P L = fpg`. So, in the case of P2 we have that p 2 SPC2P L. Also, we have that r 2 SPC3P L and s 2 SPC4P L.
In the case of P5 its stable models are the theories of CP L that contain p and do not contain q and :q. Therefore, we can conclude that p 2 SPC5P L. In the case of P6, since (p _ :p) 2 T for every logical theory T of CP L we can conclude that the only stable model of P6 is the set T heo of theorems of CP L. Therefore p 2= SPC6P L.
Consider now L = hL; `4i the 4-valued Belnap paraconsistent logic F our. Consider the program P4. Contrarily to the case of CPL, in F our it is not the case that :p; (p _ q) `4 q. Therefore we have that q; s 2= SPF4our.
Let now L = hL; `IP Li be the propositional intuitionistic logic IP L. It is well-known that q _ :q is not a theorem of IP L. Therefore, considering program P2 we have SPIP2 L = ;S`PIIP2PLL..USosi,ncgotnhterasraimlyetoidtehaefocarsperoogfrCamP LP6, wwee hcaavnecothnactlupde2=, contrarily to the case of CP L, that p 2 SPIP6 L.
In this section we discuss the use of description logics as parameter logic in the framework of parametrized logic programming. We will then illustrate the expressivity of the resulting framework to combine non-monotonic rules and ontologies.
In what follows, and for simplicity, we use description logic ALC [Schmidt-Schaubß and Smolka, 1991]. We start by briefly recalling the syntax and semantics of ALC. For a more general and thorough introduction to DLs we refer to [Baader et al., 2010]. The language of ALC is defined over countably infinite sets of concept names NC, role names NR, and individual names NI as shown in the upper part of Table 1. Building on these, complex concepts are introduced in the middle part of Table 1, which, together with atomic concepts, form the set of concepts. We conveniently denote individuals by a and b, (atomic) roles by R and S, atomic concepts by A and B, and concepts by C and D. All expressions in the lower part of Table 1 are axioms. A concept equivalence C D is an abbreviation for C v D and D v C. Concept and role assertions are ABox axioms and all other axioms TBox axioms, and an ontology is a finite set of axioms.
The semantics of ALC is defined in terms of interpretations I = ( I ; I ), which consist of a non-empty domain
I and an interpretation function I . The latter is defined for (arbitrary) concepts, roles, and individuals as in Table 1. Moreover, an interpretation I satisfies an axiom , written I j= , if the corresponding condition in Table 1 holds. If I satisfies all axioms in an ontology O, then I is a model of O, written I j= O. If O has at least one model, then it is called consistent, otherwise inconsistent. Also, O entails axiom , written O j= , if every model of O satisfies .
Given the consequence relation of ALC we can now illustrate how ALC can be used as parameter logic.
Example 2 The following program (P1) is an adaptation of an example taken from [Motik and Rosati, 2007], which uses MKNF knowledge bases to combine rules and ontologies. The scenario is about determining the car insurance premium based on various information about the driver.
N otM arried
:M arried N otM arried v HighRisk 9Spouse:> v M arried
N otM arried(x)
Note that in parametrized logic programming the combination of an ontology with a rule system can be done in a natural way, simply by adding the ontology elements as facts of the rule system. As usual in logic programming, variables in rules stand for all their possible instantiations by individuals appearing in the program.
Program P1 can be rewritten in order to remove its first rule, which is nothing but an artificial tool to overcome the impossibility of having complex DL formulas in the head of MKNF rules (in this case, having the classical negation of an atom in a head). Moreover, we may also add bodies to the facts coming from the ontology. E.g. we can add a nonmonotonic condition to the second statement of P1 above, to state that non married are only considered high-risk in non exceptional periods, obtaining P2: :M arried v HighRisk :M arried(x) not exceptionalP eriod
Let us now study the stable model semantics of this program. We should again stress that such stable model semantics does not depend on the semantics of ALC, but only on its consequence relation. If I is a 2-valued interpretation such that I(M arried(J onh)) = 1 then (I) is the least model of the following program PI2 : :M arried v HighRisk 9Spouse:> v M arried
It is clear that the smallest model of PI2 does not contain M arried(J onh), and so, such interpretation I cannot be a stable model. Therefore, every stable model must satisfy :M arried(J onh) and consequently HighRisk(J onh).
Consider now program P3 obtained by adding to P2 the following facts: p(Bill) , 9Spouse:>(Bill) , and exceptionalP eriod . Note that, although every stable model now contains :M arried(J ohn), we no longer conclude HighRisk(J onh) since we have exceptionalP eriod. Every stable model of P3 contains M arried(Bill). So, the Stable Model Semantics of P3 does not entail :M arried(Bill) nor HighRisk(Bill).
Consider now program P4 obtained by adding to P2 the facts: Spouse(Bob; Ann) , p(Bob) , and p(Ann) . Every stable model of P4 contains Discount(Bob), and so it entails Discount(Bob).
In this paper we have discussed the use of the framework of parametrized logic programming for combining nonmonotonic rules and ontologies. This approach is quite expressive since it allows complex DL axioms to appear both in the body and in the head of non-monotonic rules.
In [Gonc¸alves and Alferes, 2010] the authors show how parametrized logic programming can capture the semantics of MKNF hybrid knowledge bases [Motik and Rosati, 2010] by an appropriate choice of the parameter logic. As future work we aim to study the relation between parametrized logic programs and other frameworks for combining rules and ontologies, e.g., the DL-programs of [Eiter et al., 2008].
Ricardo Gonc¸alves was supported by FCT under project ERRO (PTDC/EIA-CCO/121823/2010).