This paper is about transformations of knowledge bases with the aid of an imperative programming language which is non-standard in the sense that it features conditions (in loops and selection statements) that are description logic (DL) formulas, and a non-deterministic assignment statement (a choice operator given by a DL formula). We sketch an operational semantics of the proposed programming language and then develop a matching Hoare calculus whose pre- and post-conditions are again DL formulas. A major di culty resides in showing that the formulas generated when calculating weakest preconditions remain within the chosen DL fragment. In particular, this concerns substitutions whose result is not directly representable. We therefore explicitly add substitution as a constructor of the logic and show how it can be eliminated by an interleaving with the rules of a traditional tableau calculus.
http://membres-liglab.imag.fr/echahed/ http://www.irit.fr/~Martin.Strecker/ Knowledge bases (KBs) are speci c forms of graphs structures that are subject to change because the world they describe changes. The question explored by this paper is: What is an adequate formalism for describing these changes, and how to reason about the e ects of changes?
Reasoning about graph transformations in full generality is hard [
In [
Work on (KB) updates [
The work described in this paper is ongoing, some results are still
preliminary. Based on previous work [
Before starting with the formal development, let us give an example of the kind of program (see Fig. 1) that we would like to write. Assume a knowledge base with objects of class A and B, and a relation r. The node n is initially connected to at least 3 objects of class A, and all objects it is connected to are of class B. Because the number of connections to A is too large, we execute a loop that selects an A-object (let's call it a) that n is connected to, and delete the r-connection between n and a. To compensate, we select an object b of class B and connect n to b. We stop as soon as the number of A-connections of n has reached 2, which is one of the post-conditions we can ascertain. 2
Our logic is a three-tier framework, the rst level being DL concepts (\TBox"),
the second level facts (\ABox", instances of concepts), the third level formulas
(Boolean combinations of facts and a simple form of quanti cation).
Concepts: We concentrate on a DL featuring concepts with simple roles and
number restrictions, similar to ALCN [
C ::= c (atomic concept) j : C (negation) j C u C (conjunction) j C t C (disjunction) j ( n r C) (at least) j (< n r C) (no more than) j C[r := RE] (explicit substitution)
Adding a universal concept > and an empty concept ? would not add expressivity, as they are equivalent to ( 0 r C) respectively (< 0 r C) for arbitrary r and C, and we will use them as shortcuts. We also write (9 r C) for ( 1 r C) and (8 r C) for (< 1 r (:C)).
The last constructor, explicit substitution [
RE ::= r (atomic role) j r (i; i) (deletion of relation instance) j r + (i; i) (insertion of relation instance)
Please note that concepts implicitly depend on the types c, r and i, which we assume mutually disjoint. A substitution can therefore never a ect an individual variable.
A set-theoretic semantics is provided by a domain an interpretation function I mapping c to a set of individuals (subsets of ), r to a binary relation of individuals (subsets of ), and i to individual elements of .
For interpretation of concepts C, negation is inductively interpreted as complement, concept conjunction as intersection and disjunction as union. I( n r C) = fx j cardfy j (x; y) 2 I(r) ^ y 2 I(C)g ng, and analogously for I(< n r C). Here, card is the cardinality of nite sets (and 0 otherwise).
For interpretation of role expressions RE, we de ne I(r (i1; i2)) = I(r) f(I(i1); I(i2))g, and I(r + (i1; i2)) = I(r) [ f(I(i1); I(i2))g.
Interpretation update I[r:=rl] modi es the interpretation I at relation name r to relation rl, thus I[r:=rl](r) = rl and I[r:=rl](r0) = I(r0) for r0 6= r. With this, we can de ne the semantics of explicit substitution by I(C[r := RE]) = I[r:=I(RE)](C).
Facts: Facts make assertions about an instance being an element of a concept, and about being in a relation. In DL parlance, facts are elements of an ABox. The type of facts is de ned as follows: f act ::= i : C (instance of concept) j i r i (instance of role) j i (:r) i (instance of role complement) j i = i (equality of instances) j i 6= i (inequality of instances)
The interpretation of a fact is a truth value, de ned by: { I(i : C) = (I(i) 2 I(C)) { I(i1 r i2) = (I(i1); I(i2)) 2 I(r) and I(i1 (:r) i2) = (I(i1); I(i2)) 2= I(r) { I(i1 = i2) = (I(i1) = I(i2)) and I(i1 6= i2) = (I(i1) 6= I(i2))
Please note that since concepts are closed by complement, facts are closed by negation (the negation of a fact is again representable as a fact), and this is the main motivation for introducing the constructors \instance of role complement" and \inequality of instances".
Formulas: A formula is a Boolean combination of facts. We also allow quanti cation over individuals i (but not over relations or concepts), and, again, have a constructor for explicit substitution.
f orm ::= ? j f act j :f orm j f orm ^ f orm j f orm _ f orm j 8i:f orm j 9i:f orm j f orm[r := RE]
The extension of interpretations from facts to formulas is standard; the interpretation of substitution in formulas is in entire analogy to concepts. As usual, a formula that is true under all interpretations is called valid.
When calculating weakest preconditions (in Sect. 4), we obtain formulas which essentially contain no existential quanti ers; we keep them as constructor because they can occur as intermediate result of computations. We say that a formula is essentially universally quanti ed if 8 only occurs below an even and 9 only below an odd number of negations. For example, :(9x: x : C ^ :(8y: y : D)) is essentially universally quanti ed.
Implication f1 ! f2 is the abbreviation for :f1 _ f2, and ite(c; t; e) the abbreviation for (c ! t) ^ (:c ! e), not to be confused with the if-then-else statement presented in Sect. 3. 3
The programming language is an imperative language manipulating relational structures. Its distinctive features are conditions (in conditional statements and loops) that are restricted DL formulas, in the sense of Sect. 2. It has a nondeterministic assignment statement allowing to select an element satisfying a fact. Traditional types (numbers, inductive types) are not provided.
In this paper, we only consider a core language with traditional control ow constructs, but without procedures. Also, it is only possible to modify a relational structure, but not to \create objects" (with a sort of new statement) or to \deallocate" them. These constructs are left for further investigation. 3.1
The type of statements is de ned by: stmt ::= Skip j select i sth f orm j delrel(i r i) j insrel(i r i) j stmt ; stmt j if f orm then stmt else stmt j while f orm do stmt 3.2
(empty statement) (assignment) (delete arc in relation) (insert arc in relation) (sequence) The semantics is a big-step semantics with rules of the form (st; ) ) 0 expressing that executing statement st in state produces a new state 0.
The rules of the semantics are given in the Fig. 2. Beware that we overload logical symbols such as 9, ^ and : for use in the meta-syntax and as constructors of f orm.
The state space is in fact identical to an interpretation function I as introduced in Sect. 2, and it is only in keeping with traditional notation in semantics that we use the symbol . We may therefore write (b) to evaluate the condition b (a formula) in state .
Most of the rules are standard, apart from the fact that we do not use expressions, but formulas as conditions. The auxiliary function delete edge modi es the state by removing an r-edge between the elements represented by v1 and v2. With the update function for interpretations introduced in Sect. 2, one de nes
= [r:= (r) f( (v1); (v2))g] (Skip; ) ) (Skip) (c1; ) ) (c1;c2; ) )
The statement select v sth F (v) selects an element vi that satis es formula F , and assigns it to v. For example, select a sth a : A^(a r b) selects an element a instance of concept A and being r-related with a given element b.
select is a generalization of a traditional assignment statement. There may be several instances that satisfy F , and the expressiveness of the logic might not su ce to distinguish them. In this case, any such element is selected, nondeterministically. Let us spell out the precondition of (SelAssT ): Here, [v:=vi] is an interpretation update for individuals, modifying at individual name v 2 i with an instance vi 2 , similar to the interpretation update for relations seen before. We therefore pick an instance vi, check whether the formula b would be satis ed under this choice, and if it is the case, keep this assignment.
In case no satisfying instance exists, the semantics blocks, i.e. the given state does not have a successor state, which can be considered as an error situation. Some alternatives to this design choice can be envisaged: We might treat a select v sth F (v) with unsatis able F as equivalent to a Skip. This would give us a choice of two rules, one in which the precondition of rule (SelAssT ) is satis ed, and one in which it is not. As will be seen in Sect. 4, this would introduce essentially existentially quanti ed variables in our formulas when computing weakest preconditions and lead us out of the fragment that we can deal with in our decision procedure. Alternatively, we could apply an extended type check verifying that select-predicates are always satis able, and thus ensure that typecorrect programs do not block. This is the alternative we prefer; details still have to be worked out. 4
We compute weakest preconditions wp and veri cation conditions vc. Both take a statement and a DL formula as argument and produce a DL formula. For this purpose, while loops have to be annotated with loop invariants, and the while constructor becomes: while ff ormg f orm do stmt. Here, the rst formula (in braces) is the invariant, the second formula the termination condition. The two functions are de ned by primitive recursion over statements, see Fig. 3. wp(Skip; Q) = Q wp(delrel(v1 r v2); Q) = Q[r := r (v1; v2)] wp(insrel(v1 r v2); Q) = Q[r := r + (v1; v2)] wp(select v sth b; Q) = 8v:(b ! Q) wp(c1; c2; Q) = wp(c1; wp(c2; Q)) wp(if b then c1 else c2; Q) = ite(b; wp(c1; Q); wp(c2; Q)) wp(whilefivg b do c; Q) = iv vc(Skip; Q) = > vc(delrel(v1 r v2); Q) = > vc(insrel(v1 r v2); Q) = > vc(select v sth b; Q) = > vc(c1; c2; Q) = vc(c1; wp(c2; Q)) ^ vc(c2; Q) vc(if b then c1 else c2; Q) = vc(c1; Q) ^ vc(c2; Q) vc(whilefivg b do c; Q) = (iv ^ :b ! Q) ^ (iv ^ b ! wp(c; iv)) ^ vc(c; iv)
Without going further into program semantics issues, let us only state the following soundness result that relates the operational semantics and the functions wp and vc: Theorem 1 (Soundness). If vc(c; Q) is valid and (c; ) ) implies 0(Q). 0, then (wp(c; Q))
What is more relevant for our purposes is the structure of the formulas generated by wp and vc, because it has an impact on the decision procedure. Besides the notion of essentially universally quanti ed introduced in Sect. 2, we need the notion of quanti er-free formula: A formula not containing a quanti er. In extension, we say that a statement is quanti er-free if all of its formulas are quanti er-free.
By induction on c, one shows: Lemma 1 (Universally quanti ed). Let Q be essentially universally quantied and c be a quanti er-free statement. Then wp(c; Q) and vc(c; Q) are essentially universally quanti ed.
We present a decision procedure for verifying the validity of essentially universally quanti ed formulas. As seen in Lemma 1, this is the format of formulas extracted by wp and vc, and as motivated by the soundness result (Theorem 1), validity of veri cation conditions is a precondition for ensuring that a program executes according to its speci cation.
Given an essentially universally quanti ed formula e, the rough lines of the procedure for determining that e is valid are spelled out in the following. Getting rid of quanti ers: 1. Convert e to an equivalent prenex normal form p, which will consist of a pre x of universal quanti ers, and a quanti er-free body: 8x1 : : : xn:b 2. p is valid i its universal closure ucl(p) (universal abstraction over all free variables of p) is. 3. Show the validity of ucl(p) by showing the unsatis ability of :ucl(p). 4. :ucl(p) has the form :8v1 : : : vk; x1 : : : xn:b. Pull negation inside the universal quanti er pre x, remove the resulting existential quanti er pre x, and show unsatis ability of :b with the aid of an extended tableau method.
Computation of prenex normal forms is standard. Care has to be taken to avoid capture of free variables, by renaming bound variables. Free variables are de ned as usual; the free variables of a substitution f [r := r (v1; v2)] are those of f and in addition v1 and v2 (similarly for edge insertion). We illustrate the problem with the following program fragment prg: select a sth a : A ; select b sth b r a ; select a sth a r b
For a given post-condition Q, we obtain
wp(prg; Q) = 8a:a : A
! 8b:(b r a)
! 8a:(a r b)
! Q
whose prenex normal form 8a1; b; a2: (a1 : A ! (b r a1) ! (a2 r b)
contains more logical variables than prg contains program variables.
! Q)
Extended tableau method { prerequisites: The tableau method takes a quanti
erfree formula f and proves its unsatis ability or displays a model. We aim at
reusing existing tableau methods (such as [
Substitution is compatible with the constructors of formulas:
?[r := re] = ? (:f )[r := re] = (:f [r := re]) (f1 ^ f2)[r := re] = (f1[r := re] ^ f2[r := re]) (f1 _ f2)[r := re] = (f1[r := re] _ f2[r := re])
The case of formulas which are facts, missing in Lemma 2, will be dealt with separately. This is due to the fact that substitution is not compatible with concepts, as will be seen in Sect. 5.2: For a given concept C, there is not necessarily a concept C0 = C[r := re]. However, substitutions can be eliminated from facts, by the equations given in Sect. 5.2.
We will refer to the equations in Lemma 2 and those in Sect. 5.2 as substitution elimination rules. We say that a substitution in a formula is visible if one of these rules is applicable; and that it is hidden if none of these rules is applicable. For example, the substitution in (x : (C1 u C2))[r := re] is visible; it is hidden in (x : (C1[r := re] u C2[r := re])) and only becomes visible after application of an appropriate tableau rule, for example of the system ALCN .
To describe our procedure, we introduce the following terminology: An ABox is a nite set of facts (interpreted as the conjunction of its facts), and a tableau a nite set of ABoxes (interpreted as a disjunction of its ABoxes). We need the following functions: { push subst takes a formula and applies substitution elimination rules as far as possible; { f orm to tab converts to disjunctive normal form and then performs the obvious translation to a tableau; { tab to f orm takes a tableau and constructs the corresponding formula. Extended tableau method { procedure: Our method is parameterized by the following interface of an implementation of your favorite tableau calculus: { a transition system T =) T 0, de ning a one-step transformation of a tableau
T to a tableau T 0. { a function sat which checks, for tableaux T that are irreducible wrt. =), whether T is satis able.
From this, we construct a restricted relation T =)r T 0, which is the same as =) provided that T does not contain visible substitutions:
T =) T 0 no visible subst in T
T =)r T 0
We also de ne a relation =)s that pushes substitutions until they become hidden:
T contains visible subst
T 0 = f orm to tab(push subst(tab to f orm(T )))
s 0
T =) T From these, we de ne the relation =)rs= (=)r [ =)s).
The extended tableau algorithm takes a formula f and computes a Tf such s that f orm to tab(f )(=)r) Tf . The result of the algorithm is sat(Tf ).
The following lemmas show that =)rs is a correct and complete algorithm for deciding the decidability of formulas with substitution provided =) is for substitution-free formulas.
Lemma 3 (Termination). =)rs is well-founded provided =) is.
To show termination of the extended algorithm, de ne { the substitution size of a formula or fact as the sum of the term sizes below its substitutions. { the substitution size of a tableau as the multiset of the substitution sizes of its facts.
Note that application of =)s leads to a reduction of the substitution size. For a well-founded measure m of =), construct a well-founded measure of =)rs as the lexicographic order of the substitution size and m.
Lemma 4 (Con uence). =)rs is con uent provided =) is. =)rs has no other critical pairs than =).
Lemma 5 (Satis ability). =)rs preserves satis ability provided =) does. The three auxiliary functions used for de ning =)s do. 5.2
We now show how substitutions can be pushed into facts.
The constructors equality and inequality are easiest to handle: { (x = y)[r := re] reduces to (x = y) { (x 6= y)[r := re] reduces to (x 6= y)
For positive resp. negative instances of roles, we have: { (x r y)[r := r (v1; v2)] reduces to (:((x = v1) ^ (y = v2))) ^ (x r y) { (x (:r) y)[r := r (v1; v2)] reduces to ((x = v1) ^ (y = v2)) _ (x (:r) y) { (x r y)[r := r + (v1; v2)] reduces to ((x = v1) ^ (y = v2)) _ (x r y) { (x (:r) y)[r := r + (v1; v2)] reduces to (:((x = v1) ^ (y = v2))) ^ (x (:r) y) whereas substitutions (x r y)[r0 := re] and (x (:r) y)[r0 := re] for r 6= r0 are the identity.
For facts of the form x : C, where C is a concept, we have the cases: { (x : :C)[r := re] reduces to x : (:C[r := re]) { (x : C1 ^ C2)[r := re] reduces to x : (C1[r := re] ^ C2[r := re]) { (x : C1 _ C2)[r := re] reduces to x : (C1[r := re] _ C2[r := re]) { (x : ( n r C))[r0 := re], for r0 6= r, reduces to x : ( n r C[r0 := re]), and similarly when replacing by < { (x : ( n r C))[r := r (v1; v2)] reduces to ite ((x = v1) ^ (v2 : (C[r := r (v1; v2)])) ^ (v1 r v2); (x : ( (n + 1) r (C[r := r (v1; v2)]))); (x : ( n r (C[r := r (v1; v2)])))) and similarly when replacing by < { (x : ( (n + 1) r C))[r := r + (v1; v2)] reduces to ite ((x = v1) ^ (v2 : (C[r := r + (v1; v2)])) ^ (v1 (:r) v2); (x : ( n r (C[r := r + (v1; v2)]))); (x : ( (n + 1) r (C[r := r + (v1; v2)])))) and similarly when replacing by < { (x : ( 0 r C))[r := r + (v1; v2)] reduces to > { (x : (< 0 r C))[r := r + (v1; v2)] reduces to ? { Pathological case (x : C[sbst1])[sbst2]: lift inner substitution to (x : C)[sbst1][sbst2], then apply the above. 6
This paper proposes a language for rewriting knowledge bases, and methods for reasoning about the correctness of these programs, by means of a Hoare-style calculus. DL formulas are directly integrated into the statements of the programming language. The veri cation conditions extracted from these programs has been shown to be decidable, by a modular extension of existing tableau algorithms.
The work described here is still preliminary, in several respects, and the following points indicate directions for future investigations: { We are in the process of coding the theory in the Isabelle proof assistant.
Some parts of the proofs of Sect. 4 and most of Sect. 5.1 still has to be done. The purpose is to obtain a framework that will allow us to experiment more easily with variations of the logic. { We have currently focused on the logic ALCN . It is interesting to consider both less expressive logics (which o er more space for optimizations) and more expressive logics (to explore decidability questions). The process described in Sect. 5.1 is rather generic, but it remains to be seen whether more expressive DLs, featuring more complex role expressions, can be accommodated. { In any case, the proof procedure sketched in Sect. 5 is rather of a theoretical than a practical value; an e cient implementation should not convert between formulas and tableaux as indiscriminately as suggested there, but apply propagation of substitutions locally. { In a similar vein, it would be interesting to implement a transformation engine on the basis of the language described here, also with the purpose of evaluating the practical expressiveness of the language on larger examples.