Constructing Formally Verified Reasoners for the ALC Description Logic

Constructing Formally Verified Reasoners for the ALC Description Logic M. J. Hidalgo, J. A. Alonso, F. J. Mart´ın and J. L. Ruiz 1 ,2 Department of Computer Sciencs University of Seville Sevilla, Spain Abstract Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. Recently, its importance has been increased since they are used as a basis for the Ontology Web Language (OWL) used for the Semantic Web. In previous work, we have developed in PVS a generic framework for reasoning in the ALC description logic, proving its termination, soundness and completeness. In this paper we present the construction, from the generic framework, of a formally verified generic tableau– based algorithm for checking satisfiability of ALC –concepts. We do it using a methodology of refinements to transfer the properties from the framework to the algorithm. We also obtain some verified reasoners from the algorithm by a process of instantiation. Keywords: Semantic Web, Description Logics, Verification, Formal Methods. 1 Introduction For processing knowledge in the Semantic Web, reasoners of Description Logics (DLs) such as RACER, Pellet and FaCT++ [6,11,12] are being used. Description Logics [3] are a family of logics used to represent conceptual and terminological knowledge. Among these, the ALC logic is a ground logic, which can be extended to the more expressive logic SHOIN, which corresponds to the Ontology Web Language. Formally verifying the reasoners for DLs could increase their reliability and so that of the Semantic Web. However, formal verification of properties of reasoners for DLs is a time and resource consuming task. Moreover, if we carry out the formal verification of different reasoners for a logic, we will probably have to solve analogous problems for each one. 1This research was partially funded by Spanish Ministry of Education and Science under grant TIN2004– 03884 and Feder funds 2Email: mjoseh,jalonso,fjesus,[email protected] In [1], we have formalized a generic framework for checking satisfiability of ALC – concepts in the PVS verification system [9]. The goal of this work is to construct reasoners for the ALC –description logic from a generic framework in such a way that the verified properties of the generic framework are transferred to the reasoners. For this, in order to transfer the correctness of the framework to the reasoners we apply the type and operator refinement techniques shown in [2]. The main phases of the process we have followed, whose details we explain below, are shown in Figure 1. Generic Framework in PVS PropertiesGeneric Algorithm 1 Generic Algorithm 2 Properties PropertiesReasoner 1a Reasoner 1b Reasoner 2a Reasoner 2b Properties Properties Properties Properties Fig. 1. The roadmap (i) Generic framework (in the figure, the boxes). In this phase, which will be summarized in Section 3, we formalize in PVS a generic specification (using generic types) for checking satisfiability of ALC –concepts. We prove termination, soundness and completeness. The features of the specification make it feasible that the proofs of its properties are close to the same ones in the usual literature. It should be noted that, in general, the most difficult proof is that of termination. (ii) Generic algorithm (in the figure, the octagons). In this second phase, described in Section 5, we implement in PVS a generic algorithm corresponding to the previous specification, in such a way that the correctness properties of this algorithm are based on the same properties already proved for the generic framework. For this purpose, we use the methodology of refinements described in Section 4. In this step, the algorithm is generic in the sense that the strategy of application of completion rules is not determined. That is, the specified algorithm depends on a selection function coding the strategy. The correctness of the algorithm has been proved, assuming some generic hypotheses about the nondetermined selection function. (iii) Reasoners (in the figure, the ellipses). In the last phase, described in Section 6, we develop reasoners for the ALC logic in PVS, considered as instances of the generic algorithm. For this, it suffices to instantiate the strategy of application of completion rules by a selection function. It should be emphasized that in order to prove the correctness of these reasoners, we only have to prove instances of the assumed hypotheses, for each concrete selection function. To develop our work, we have chosen the PVS system. This system combines an expressive specification language with an interactive theorem prover. Also, although the PVS specification language has been designed to be expressive rather than executable, a wide fragment of PVS is executable by generating Common Lisp code from PVS, that can be evaluated through the PVSio environment [8]. 2OverviewofPVS PVS (Prototype Verification System) [9] is a general–purpose environment for developing specifications and proofs. In this section, we present a brief description of the PVS language and prover, introducing some of the notions used in this paper. The PVS specification language is built on a classical typed higher–order logic with the basic types bool,nat,int, in addition to the function type constructor [D -> R] and the product type constructor [A, B]. The type system is also augmented with dependent types and abstract data types. A feature of the PVS specification language are predicate subtypes: the subtype {x:T | p(x)}consists of all the elements of type Tverifying p. The notation (A) is used to indicate the subtype {x:T | A(x)}. Predicate subtypes are used for constraining domains and ranges of functions in a specification and, therefore, for defining partial functions. In general, type-checking with predicate subtypes is undecidable. Therefore, the type-checker generates proof obligations, called type correctness conditions (TCCs). This TCCs are either discharged by specialized proof strategies or proved by the user. In particular, for defining a recursive function, it must be ensured that the function terminates. For this purpose, in the definition of a recursive function, the user has to provide a measure function. This generates a TCC stating that the measure function applied to the arguments decreases with respect to a well–founded ordering in every recursive call. A built-in prelude and loadable libraries provide standard specifications and proved facts of a large number of theories. PVS specifications are packaged as theories that can be parametrized with respect to types and constants. The definitions and theorems of a theory can then be used by another theory by importing it. 3 A generic framework for checking satisfiability of ALC –concepts The goal of this section is to present a summary of a PVS formalization of a generic framework for checking satisfiability of ALC –concepts, in which different tableaux–based algorithms can be placed. A more detailed description of this formalization, can be seen in [1] and the whole formalization is available at http://www.cs.us.es/~mjoseh/alc/. Since one of our goals in the development of the formalization of the generic framework is to obtain a high degree of generality, we have specified the relations in a declarative way, instead of by the corresponding function. Another goal of our development is to obtain PVS proofs closely resembling the proofs that we can find in the usual literature, in such a way that the complexity of a PVS proof stems from the proof itself, and not from the additional complexity introduced by the use of some specific data structure. For that reason, we have mainly used the type of finite sets. We first describe the basic components of the ALC logic, and we show below how we have formalized in PVS a generic framework for tableau–based algorithms for this logic. We present the ALC logic along with the corresponding description of its specification in PVS. Let NC be a set of concept names and NR be a set of role names.Thesetof ALC –concepts is built inductively from these names as described by the following grammar, where A∈NC and R∈NR C::= A|¬C|C1C2|C1C2|∀R.C |∃R.C The set of ALC –concepts can be represented in PVS as a recursive datatype, using the mechanism for defining abstract datatypes [10], and specifying the constructors, the accessors and the recognizers. To introduce the assertional knowledge, let NI be a set of individual names. Given individual names x, y ∈NI, a concept Cand a role name R, the expressions x:Cand (x, y): Rare called assertional axioms.AnABox Ais a finite set of assertional axioms. We specify in PVS the assertional axioms by a datatype and the ABox by a type assertional_ax: DATATYPE BEGIN instanceof(left:NI, right:alc_concept) : instanceof? related(left:NI, role:NR, right:NI) : related? END assertional_ax ABox: TYPE = finite_set[assertional_ax] The semantics of description logics is defined in terms of interpretations. An ALC –interpretation Iis a pair I=(Δ I,·I), where ΔIis a non–empty set called the domain,and·Iis an interpretation function that maps every concept name Ato a subset AIof ΔI, every role name Rto a binary relation RIover ΔIand every individual xto an element of ΔI. We represent in PVS an interpretation Ias a structure that contains the domain of Iand the functions that define the interpretation of concept names, role names, and the individuals interpretation: NONEMPTY_TYPE = [# int_domain: (nonempty?[U]), int_names_concept: [NC -> (powerset(int_domain))], int_names_roles: [NR -> PRED[[(int_domain),(int_domain)]]], int_names_ind: [NI -> (int_domain)] #] The interpretation function is extended to non-atomic concepts as follows (¬D)I=Δ I\DI (C1C2)I=CI 1∩CI 2 (C1C2)I=CI 1∪CI 2 (∀R.D)I={a∈ΔI:(∀b∈ΔI)[(a, b)∈RI→b∈DI]} (∃R.D)I={a∈ΔI:(∃b∈ΔI)[(a, b)∈RI∧b∈DI]} The interpretation Iis a model of a concept Cif CI=∅. Thus, a concept Cis called satisfiable if it has a model is_model_concept(I,C): bool = nonempty?(int_concept(C,I)) concept_satisfiable?(C): bool = EXISTS I: is_model_concept(I,C) The interpretation Isatisfies the assertional axiom x:Cif xI∈CIand satisfies (x, y): Rif (xI,yI)∈RI.Itsatisfies the ABox Aif it satisfies every axiom in A. In that case, Ais called satisfiable and Iis called a model of A. We have made the PVS formalization of the above definitions, in a generic way using the PVS set theory and its capability of managing the existential and universal quantifiers. In order to decide the satisfiability of an ALC –concept, a tableau algorithm tries to prove the satisfiability of a concept Cby attempting to explicitly construct amodelofC. This is done considering an individual name x0and manipulating the initial ABox {x0:C}, applying a set of completion rules. In this process, we consider concepts in negation normal form (NNF), a form in which negations appear only in front of concept names. This does not impose any restriction since it is easy to specify a PVS function such that, for each ALC –concept, computes another equivalent in NNF form. An ABox Acontains a clash if, for some individual name x∈NI and concept name A∈NC,{x:A, x:¬A}⊆A.Otherwise,Ais called clash–free contains_clash(AB): bool = EXISTS Aa: member(Aa,AB) AND instanceof?(Aa) AND alc_atomic?(right(Aa)) AND member(instanceof(left(Aa), alc_not(right(Aa))), AB) To test the satisfiability of an ALC –concept Cin NNF, the ALC –algorithm works starting from the initial ABox {x0:C}and iteratively applying the following completion rules: →:if x:CD∈Aand {x:C, x:D} ⊆A then A→ A∪{x:C, x:D} →:if x:CD∈Aand {x:C, x:D}∩A=∅ then A→ A∪{x:E}for some E∈{C, D} →∃:if x:∃R.D ∈Aand there is no ywith {(x, y): R, y:D}⊆A then A→ ∃A∪{(x, y): R, y:D}for a fresh individual y →∀:if x:∀R.D ∈Aand there is a ywith (x, y): R∈Aand y:D∈A then A→ ∀A∪{y:D} It stops when a clash has been generated or when no rule is applicable. In the latter case, the ABox is complete and a model can be derived from it. The algorithm answers “Cis satisfiable” if a complete and clash–free ABox has been generated. We have formalized these completion rules following a declarative style, defining them in PVS as binary relations between ABoxes. For example, A1→1A2if there exists an assertional axiom x:CDin A1such that x:C∈A 1,x:D∈A 1and A2=A1∪{x:C} or_step_1(AB1, AB2): bool = EXISTS Aa: member(Aa, AB1) AND instanceof?(Aa) AND alc_or?(right(Aa)) AND NOT member(instanceof(left(Aa),conc1(right(Aa))),AB1) AND NOT member(instanceof(left(Aa),conc2(right(Aa))),AB1) AND AB2 = add(instanceof(left(Aa),conc1(right(Aa))),AB1) Once the rules have been specified in this way, we define the successor relation on the ABoxes type: A1→A 2if A1does not contain a clash and A2is obtained from A1by the application of a completion rule successor(AB2,AB1): bool = (NOT contains_clash(AB1)) AND (and_step(AB1,AB2) OR or_step_1(AB1,AB2) OR or_step_2(AB1,AB2) OR some_step(AB1,AB2) OR all_step(AB1,AB2)) It should be noted that we have specified the non-deterministic rule →by two binary relations (or_step_1 and or_step_2), one for each component. Taking into account that the completion process can be seen as a closure process, we say that the ABox A2is an expansion of the ABox A1if A1∗ →A 2,where ∗ →is the reflexive and transitive closure of →. To illustrate the completion process, the following example shows the application of some completion rules to an initial ABox {x0:C} Example 3.1 Let Cbe the concept ∀R.D (∃R.(DE)∃R.(DF)). Then, A0:= {x0:∀R.D (∃R.(DE)∃R.(DF)) ∗ →A 1:= A0∪{x0:∀R.D, x0:∃R.(DE),x 0:∃R.(DF)} →A 2:= A1∪{(x0,x 1): R, x1:DE} →A 3:= A2∪{x1:D} Once defined the expansion relation, we use it to specify the notions of completeness and consistency. An ABox Ais complete if it has not any successor and is consistent if it has a complete and clash–free expansion. Similarly, a concept C is consistent if the initial ABox {x0:C}is consistent complete(AB): bool = FORALL AB1: NOT successor(AB1, AB) is_consistent_abox(AB): bool = EXISTS AB1: is_expansion(AB)(AB1) AND complete_clash_free(AB1) is_consistent_concept(C): bool = is_consistent_abox(singleton(instanceof(x_0,C))) where complete_clash_free(A)holdsiftheABoxAis both complete and clash– free. This definition is the PVS specification of a generic framework for deciding satisfiability of ALC –concepts. It should be pointed out the two types of non– determinism in it: the way in which the rule →is applied (“don’t know” nondeterminism); and the choice of which rule to apply in each step and to which axiom (“don’t care” non-determinism). We have established in [1] the correctness of this specification, proving its termination, soundness and completeness. 4 Methodology of refinements In this section we present a sketch of the type and operator refinement techniques developed in PVS in order to relate different specifications of the same notion. The point is that if we want to prove properties about a program, the development of the formal proof will strongly depend of the used datatypes as well as the concrete implementation of it. Thus, the idea is to verify the desired properties for a generic specification of this program and that the verified properties can be transferred to it. For this, based on the idea of refinement of data types used by A. Dold [5]and C. B. Jones [7] we have built in PVS a theory establishing the general notions of refinements and its main properties (see [2]). Given types Tand R,wesaythata data refinement of the type Tby the type Ris a surjective application f:R→T f: VAR [R->T] is_ refinement?(f): bool = FORALL (t:T): EXISTS (r:R): f(r) = t Intuitively, this function provides the relationship between abstract values (T) and their representations (R). It is clear that there is at least one representation, not necessarily unique, for any abstract value. Also, we can see that a type can be refined stepwise by sequential composition of refinements. In that sense, we prove in PVS that, if f:R→Tis a data refinement of Tby Rand g:Q→Ris a data refinement of Rby Q,thenf◦g:Q→TisadatarefinementofTby Q. With respect to the refinements of operators or functions, let us consider an operator op :T1→T2and let us suppose that we have the data refinements given by the functions f1:R1→T1and f2:R2→T2. We say that the operator opref :R1→R2is a refinement of op if the following diagram commutes: T1 op −→ T2 ↑↑ f1|f2| || R1 opref −→ R2 op: VAR [T1 -> T2] op_ref: VAR [R1 -> R2] is_refinement_op?(op,op_ref): bool = FORALL r1: op(f1(r1))=f2(op_ref(r1)) In essence, we require that opref has the same behavior as op.Themostimportant feature of this definition is that it makes possible to transfer the properties of the operator op to the operator opref. For example, we prove that the well– foundedness of a relation can be transferred through the refinements refinement_preserve_wf: LEMMA is_refinement_op?(rel,rel_ref) AND well_founded?(rel) IMPLIES well_founded?(rel_ref) In a more general way, let us suppose that we have established a correctness theorem for op, in terms of pre and post conditions. That is, a theorem like (∀y∈T1)[φ(y)⇒ρ(y,op(y))] where φis the precondition and ρis the postcondition. Then, if opref ,φ ref and ρref are refinements of op, φ and ρ, respectively, we have proved that (∀x∈R1)[φref (x)⇒ρref (x, opref (x))] which is just the correctness theorem corresponding to opref . And this has been proved in a general way without no specific assumptions about φ, ρ and op. In order to illustrate the above idea, we show how we have formalized a refinement of finite sets by lists. Let us consider a data refinement f:R→T.From this, we specify a data refinement of type “finite sets with elements in T”bythe type “lists with elements in R”, by the function c(f):list[R] →finite set[T], defined as follows c(f)(l: list[R]): RECURSIVE finite_set[T] = CASES l OF null: emptyset, cons(x, l1): add(f(x), c(f)(l1)) ENDCASES MEASURE length(l) To build refinements corresponding to the operations over finite sets we use operations over lists “simulating” the behaviour of analogous operations on finite sets. For example, the built–in operations null?,cons and append are refinements of empty?,add and union, respectively. As for the membership relation, it can be noticed that if fis injective, the predicate member for lists is a refinement of the predicate member for finite sets. Finally, regarding the construction of a refinement on a specification, we take into account that a specification of an algorithm is normally built combining some other specifications of operators. Hence, for constructing a refinement of a specification of an algorithm it suffices to construct a refinement of each operator used in it, and to replace it. In that sense, we prove that if op1ref and op2ref are refinements of op1 and op2, respectively, then op2ref ◦op1ref is also a refinement of op2◦op1. 5 Generic algorithms for checking satisfiability of ALC – concepts This section is devoted to present the construction of a generic algorithm corresponding to the specification of the generic framework that we have described in Section 3. In addition, our purpose is to do it in such way that its termination, soundness and completeness can be deduced from the corresponding properties of the generic framework. For this, we will use the methodology of refinements explained in Section 4. It should be noted that the specification of the generic framework cannot be transformed into an algorithm by composition of refined operators for each of the operators composing this specification. The main reason is that in the generic framework, the searching process that the algorithm has to carry out in the space E(C) of the expansions of the initial ABox {x0:C}is not specified. So, in the process of construction of the algorithm we have to concretize how to carry out the search. Also, we have to consider the following facts: (i) It is necessary to use evaluable data types. For this, we have to refine, among others, the type used to represent ABoxes (finite sets) by another evaluable type (in this case, lists). (ii) It is necessary to define evaluable specifications of the predicates used for recognizing if an ABox is complete and clash-free. (iii) Since we will construct a recursive algorithm, it is necessary to have a well– foundness relation in E(C), that provides a measure function for proving its termination. Finally, we have obtained some concrete reasoners by instantiation of noninterpreted types and of the function which coded the strategy to select the rule to apply in each step. It is worth pointing out that this makes the formal verification of the fundamental properties of the reasoners easier, since this is reduced to prove the hypotheses assumed on the generic function that codes the selection strategy. We would like to point out some lines for future work. We plan to continue this work following several research lines. First, we will extend the ALC –reasoners to manage concept satisfiability with respect to terminological Boxes. Second, we will deal with more specific algorithms which optimize the performing by richer data structures. Also, we are interested in extending the reasoners for the ALC logic to other description logics, incrementally approaching us to the description logic SHOIN, which is the description logic corresponding to OWL–DL. References [1] J. A. Alonso, J. Borrego, M. J. Hidalgo, F. J. Mart´ın and J. L. Ruiz, A formally verified prover for the ALC description logic,LNCS4732, Springer (2007), 135–150. [2] J. A. Alonso, J. Borrego, M. J. Hidalgo, F. J. Mart´ın and J. L. Ruiz, Verification of the Formal Concept Analysis, RACSAM (Revista de la Real Academia de Ciencias), Serie A: Matem´aticas 98 (2004), 3–16. [3] F. Baader, D. McGuiness, D. Nardi and P. Patel–Schneider, The Description Logic Handbook: Theory, Implementation and Applications, Cambridge University Press (2003). [4] F. Baader and B. Hollunder, A Terminological Knowledge Representation System with Complete Inference Algorithms., PDK (1991), 67–86. [5] A. Dold, “Formal Software Development using Generic Development Steps, “ Ph.D. thesis, Ulm University, 2000. [6] V. Haarslev and R. M¨oller, RACER System Description,LNCS2083, Springer (2001), 701–705. [7] C. B. Jones, Systematic Software Development using VDM, Prentice–Hall International, (1990). [8] C. Mu˜noz, PVSio Reference Manual Version 2.b, National Institute of Aerospace (2005). [9] S. Owre, J. M. Rushby and N. Shankar, PVS: A Prototype Verification System, LNAI 607, Springer 1992, 748–752. [10] S. Owre and N. Shankar, Abstract Datatype in PVS, Computer Science Laboratory, SRI International, (1997). [11] E. Sirin and B. Parsia, Pellet System Description, Proceedings of the 2006 International Workshop on Description Logics (DL2004), CEUR Workshop Proceedings 189 (2006). [12] D. Tsarkov and I. Horrocks, FaCT++ Description Logic Reasoner: System Description, LNAI 4130, Springer (2006), 292–297.