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.
Contribution The question explored in this paper is: What is an adequate formalism for describing modi cations of Knowledge Bases (KBs), and how to reason about the e ects of these modi cations?
Let us x some terminology: In this paper, a KB is perceived as a graph structure, consisting of nodes and binary relations between these nodes. A KB transformation modi es this graph structure, by inserting or deleting arcs in the graph (and by adding or deleting nodes, but this aspect is not addressed in this paper because it would need mechanisms analogous to memory allocation and deallocation in traditional programming languages).
A KB can be seen as a model of a formula of a particular logical language. For expressive logics, typical transformation problems (see further below) become undecidable. We therefore cut down the problem to rather inexpressive logics, in this case a variant of the Description Logic ALCQ.
A transformation of a KB induces a transformation of predicates true about the KB: If predicate P is true for a KB k, which predicate P 0 is true for the ? Part of this research has been supported by the Climt project (ANR-11-BS02-016). transformed KB k0? The answer to such a question depends on at least two factors: the language used for de ning transformations, and the logical formalism for reasoning about them. Our contribution consists in { a proposal for a transformation language similar to a traditional imperative language, but endowed with some non-standard constructs (a nondeterministic assignment operator and conditional and loop statements where expressions are replaced by formulas). In spite of these features, transformations are e ectively computable. The extension of ALCQ we use is de ned in Sect. 2, the programming language in Sect. 3. { a sound and decidable Hoare-style calculus for reasoning about transformations written in this language.
The approach is rather standard: we compute weakest preconditions (WPs) by structural recursion over the statements of the transformation language, see Sect. 4. Unfortunately, it turns out that the logic ALCQ is not directly closed wrt. substitutions that have to be carried out when computing WPs. We therefore add a new constructor for substitutions to the logic, and show how it can be eliminated in a tableau calculus (in Sect. 5).
Related work 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 A or 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. The resulting transformation is depicted in Fig. 2. One also sees that the language is too weak to express other properties, for example that the total number of arcs is preserved by the transformation.
vars n, a, b; /* Pre: n : (
3 R A) u (8 R (A t B)) */ while ( n : (> 2 R A) ) do f /* Inv: n : ( 2 R A) u (8 R (A t B)) */ select a sth a : A ^ (n R a); delete(n R a); select b sth b : B ; add(n R b) g /* Post: n : (= 2 R A) u (8 R (A t B)) */ 4 http://www.irit.fr/~Martin.Strecker/Publications/dl_transfo2013.html
Our logic is a three-tier framework, the rst level being DL concepts, the second level facts, 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 ALCQ [
C ::= ? (empty concept) j 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)
We de ne the universal concept > as :? and 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 and 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. We overload the notation ? for empty concepts and the Falsum.
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.
The type of statements is de ned by: stmt ::= Skip (empty statement) j select i sth f orm (assignment) j delrel(i r i) (delete arc in relation) j insrel(i r i) (insert arc in relation) j stmt ; stmt (sequence) j if f orm then stmt else stmt j while f orm do stmt
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. 3. 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 a function mapping individual variables to individuals in the semantic domain ; concepts to sets of individuals, and so forth. It is therefore 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 delete edge v1 r v2
= [r:= (r) f( (v1); (v2))g] and similarly generate edge v1 r v2
= [r:= (r)[f( (v1); (v2))g]
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. (Skip; ) ) (Skip) (c1; ) ) (c1;c2; ) ) (Seq) 0 = delete edge v1 r v2 (delrel(v1 r v2); ) ) 0 (EDel) 0 = generate edge v1 r v2
0 (insrel(v1 r v2); ) ) (EGen) (select v sth b; ) ) 9vi:( 0 = [v:=vi] ^ 0(b))
0 (SelAssT ) (b) (c1; ) )
0 (if b then c1 else c2; ) ) 0 (If T ) : (b) (c2; ) )
0 (if b then c1 else c2; ) ) 0 (If F ) (b) (c; ) ) (while b do c; ) ) 00 (while b do c; 00) ) 0 0 (W T )
: (b) (while b do c; ) ) (W F ) 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. 4. 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 for the DL fragment under consideration here. 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. 5 5.1
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 a consequence of substitution not being 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 ALCQ.
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. For lack of space, we cannot treat all constructors.
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.