Changes between Version 1 and Version 2 of IdsAdiTemplateAxiomatizationTools

Timestamp:

11/05/09 21:45:30 (15 years ago)

Author:

jowik (IP: 193.212.132.34)

Comment:

--

IdsAdiTemplateAxiomatizationTools

@@ -16 +16 @@
 ''This page provides a walkthrough of how to develop axioms (interpretation rules) for ISO 15926 templates, aided by software tools. The aim is for this page to eventually provide a useful introduction and tutorial.''
 
+= Basic =
+== Template signatures ==
+Example: !IsCustodianOf
+|| Order || Role name || Role type       ||
+||     1 || Custodian || Adult person    ||
+||     2 || Child     || Person          ||
+||     3 || Type      || !CustodyRelation ||
+
+Example: !ClassificationOfIndividual
+|| Order || Role name  || Role type          ||
+||     1 || Individual || !PossibleIndividual ||
+||     2 || Class      || !ClassOfIndividual  ||
+== Template axioms ==
+
+For !IsCustodianOf an axiom could say, the ''Parent'' stands in a
+parenthood relationship of type ''CustodyRelation'' to the ''Child''.
+
+For !ClassificationOfIndividual (in Part 7), the rule is as follows.
+{{{
+ClassificationOfIndividual(x1, x2) <->
+  PossibleIndividual(x1) &            
+  ClassOfIndividual(x2) &       
+  ClassificationTemplate(x1, x2) .
+}}}
+(We use Prover9 syntax to express the formula, so we can use it as-is
+in that proof tool.)
+
+= Some reasons why we need templates =
+ - Simplify use of ISO 15926 representations
+         - Expressions in the language of ISO 15926-2 tend to be
+     verbose. The entity types are also hard to grasp. With templates,
+     the logical design work can be left to modelling experts.
+ - A uniform approach to knowledge capture
+         - Templates are always ''statement forms''. Any valid template
+     instance corresponds to a statement.
+ - Simplify use of n-ary predicates 
+         - Due to its basis in standard Description Logic, OWL has only
+     unary and binary predicates
+         - Templates are a convenient way to introduce n-ary predicates,
+     without introducing too much semantic confusion (cf. W3C's
+     [http://www.w3.org/TR/swbp-n-aryRelations/#useCase3 Purchase] example, for which instances are purchases, not facts)
+ - Convenient exchange of representations
+         - Templates are comparable to SQL table definitions, but the most
+     interesting roles (columns) are typed using reference data
+ - Convenient data transfer
+         - It's easy to instantiate templates and move a payload
+
+All of the above are good, but not exactly revolutionary. Arguably,
+the greatest advantage of templates is found in the interpretation of
+template rules as logical axioms.
+
+ - Basis in precise modelling
+         - Templates are expressed in a clearly defined limited first-order
+     logic, whose properties are well known
+ - Definitions can be tested for compliance with ISO 15926-2
+         - This is much of today's topic
+ - Templates can be tested for mutual consistency
+ - Payloads of data can be tested for internal consistency
+ - Complex templates can be defined in terms of simpler templates
+ - Libraries of templates can be tested for internal consistency
+ - We can check that templates are well-defined in the sense of always
+   reducing to a unique expression in the basic, Part 2 language
+
+= Template Expander: Intro, and a minimal example =
+The
+[https://www.posccaesar.org/svn/pub/TemplateExpander/applet/template-expander.html Template Expander] is a tool for working with template design. It
+was written in Java by [http://heim.ifi.uio.no/martingi/ Martin Giese]. Development was funded by DNV
+IRM. 
+== Java library ==
+Using the Java library
+([https://www.posccaesar.org/svn/pub/TemplateExpander/cmdline/template-expander.jar template-expander.jar]), expansion of template
+rules can be built into ISO 15926 applications.
+
+The code is available as free software, with a BSD-type
+[https://www.posccaesar.org/svn/pub/TemplateExpander/LICENSE LICENSE]:
+{{{
+Copyright (c) 2009, DNV Information Risk Management 
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without 
+modification, are permitted provided that the following conditions are met:
+  
+  * Redistributions of source code must retain the above copyright 
+    notice, this list of conditions and the following disclaimer.
+  * Redistributions in binary form must reproduce the above copyright 
+    notice, this list of conditions and the following disclaimer in the 
+    documentation and/or other materials provided with the distribution.
+  * Neither the name of DNV Information Risk Management nor the names of its 
+    contributors may be used to endorse or promote products derived from 
+    this software without specific prior written permission.
+  
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 
+(etc etc)
+}}}
+== Java applet ==
+At
+[https://www.posccaesar.org/svn/pub/TemplateExpander/applet/template-expander.html Template Expander], a Java applet has been provided with a heading,
+an introduction, and IDS-ADI and DNV logos.
+=== Window "Template Definitions" ===
+Enter all template definitions into this window.
+
+Upon initialization, the templates defined in the
+[https://www.posccaesar.org/svn/projects/ISO15926/Part7-Apr-2009_delivery/ISO15926-7_TS.pdf Part 7 April 2009 draft] 
+are loaded here, in Prover9 format.
+
+For a toy example, consider a two-place template "!SiblingOf(x, y)" for
+expressing that people are siblings. Intuitively, "!SiblingOf(Alfred,
+Betty)" should mean that Alfred and Betty are siblings. Template
+signature:
+|| Order || Role name || Role type ||
+||     1 || Sibling A || Person    ||
+||     2 || Sibling B || Person    ||
+
+Note that the signature doesn't say anything about how role-fillers
+are related. For that, we assume our ontology (our reference data
+library) defines a relation ''hasChild'', holding between parents and
+their children. We use this in the template axiom.
+
+{{{
+SiblingOf(x, y) <->
+  Person(x) & Person (y) &
+  exists z ( Person(z) &
+             hasChild(z, x) &
+              hasChild(z, y)) .
+}}}
+(Note the final ".", which is required by Prover9.)
+
+(for an ISO 15926 application using reference classes, we'd have in
+line 2, e.g.,
+{{{
+ClassificationTemplate(x, Person) & ...
+}}}
+)
+=== Window "Input Formula" ===
+This window is for entering atomic/ground statements using the
+template language.
+
+Enter a single formula here (without a final "."). If you wish to test
+more than one template instance, then express it as a conjunction,
+with "&".
+{{{
+SiblingOf(Alfred, Betty)
+}}}
+
+We need to follow the restrictions on names of variables, individuals,
+and so forth given by Prover9. 
+=== Button "Expand" ===
+With our toy example, the ''Expand'' button returns this:
+{{{
+  Person(Alfred)
+& Person(Betty)
+& exists z (Person(z) & hasChild(z, Alfred) & hasChild(z, Betty))
+}}}
+==== Checkbox "Skolemize result" ====
+If we choose to ''skolemize'', new terms are created to satisfy the
+''exists'' quantifiers:
+{{{
+  Person(Alfred)
+& Person(Betty)
+& Person(cz0)
+& hasChild(cz0, Alfred)
+& hasChild(cz0, Betty)
+}}}
+This can be easily converted into XML or RDF, for inspection in
+various tools; see below ([id:b2f8cdce-0346-430a-a576-cf9ba747f356
+ex. 1], [id:47904671-d234-4ffa-946b-c0934b49c5ad ex. 2]). Visualized
+in [http://semweb.salzburgresearch.at/apps/rdf-gravity/ RDF-Gravity],
+an RDF file can appear follows.
+
+[[Image(AlfredBetty-tpl-instances.png)]]
+
+= Prover9: Intro, and the minimal example again =
+== The program ==
+The Prover9 theorem prover, and its companion Mace4 for finding
+counterexamples, have a convenient graphical user interface that makes
+it more usable than other provers that are available.
+
+NB. Prover9 works for full first-order logic. This is much more
+permissive than what is allowed for templates -- we can make more
+expressive statements. This means that application of Prover9 can be
+used to test many kinds of relationships that can not be expressed in
+templates themselves.
+=== Symbol list: Logical operators ===
+Prover9 is quite picky about symbols.
+|| Operator                   || Symbol ||
+|| true                       || $T     ||
+|| false                      || $F     ||
+|| negation                   || -      ||
+|| disjunction                || \mid   ||
+|| conjunction                || &      ||
+|| implication                || ->     ||
+|| equivalence                || <->    ||
+|| universal quantification   || all    ||
+|| existential quantification || exists ||
+|| equality                   || =      ||
+|| negated equality           || !=     ||
+=== Window "Assumptions" ===
+This is where the template axioms go. We can test for well-formedness.
+Incidentally, this is also done in the Template Expander, so if you
+get expansions there, your definitions should be good for Prover9 too.
+
+Let's enter in our example from above.
+{{{
+SiblingOf(x, y) <->
+  Person(x) & Person (y) &
+  exists z ( Person(z) &
+             hasChild(z, x) &
+             hasChild(z, y)) .
+
+SiblingOf(Alfred, Betty) .
+}}}
+We can click the ''Well Formed?'' button to check that we haven't made a
+syntax error. 
+=== Window "Goals" ===
+==== Proof ====
+With the template definition and our instance, we can prove that Betty
+is a sibling of Alfred -- since the order of conjuncts in the template
+axiom is insignificant. We click the button ''Start'' under "Proof
+Search".
+{{{
+SiblingOf(Betty, Alfred) . 
+}}}
+We can also show information about the role-fillers Alfred and Betty
+that is implied by the template definition.
+{{{
+Person(Betty) .
+}}}
+==== Disproof ====
+There's also information that ''doesn't'' follow from our assumptions.
+In many cases, Prover9 can explain that this is so by generating a
+counterexample. For the following, click the button ''Start'' under
+"Model/Counterexample Search". (The proof search should fail since we
+haven't entered any assumption to the effect that Alfred has a child.)
+{{{
+exists x ( hasChild (Alfred, x)) .
+}}}
+The converse is of course provable.
+{{{
+exists x ( hasChild (x, Alfred)) .
+}}}
+= Rahul's examples =
+== Properties of individuals. Preparation ==
+In email 2009-11-04, Rahul Patil (Bentley) proposes templates for
+properties of individuals. He provides two alternatives -- "Option 1"
+and "Option 2".
+
+To prepare the templates for testing in the Template Expander and
+Prover9, we first edit the formulae to replace symbols "^" with "&",
+and the mirror-image existential quantifier with "exists". 
+
+== Option 1 ==
+=== Prepare axiom ===
+The template axiom is the following.
+{{{
+PropertyOfIndividual(x1, x2, x3) <-> 
+  PossibleIndividual(x1) &
+  Property(x2) & 
+  ClassOfIndirectProperty(x3) &
+  exists u ( IndirectPropertyTriple(u, x1, x2) & 
+             ClassificationTemplate(u,x3))
+}}}
+To check that the definition is syntactically adequate, we open the
+Template Expander and add the definition to the end of the Template
+Definitions field. 
+=== Enter sample instance ===
+We then enter the example instance given by Rahul as an Input Formula.
+
+Note that the input needs to be slightly rewritten to conform to the
+Prover9 requirements on permissible terms. We replace
+{{{
+PropertyOfIndividual( #s-101, 60bar, Maximum Working Pressure )
+}}}
+with
+{{{
+PropertyOfIndividual(s101, bar60, MaximumWorkingPressure)
+}}}
+This is no major issue, since we're only testing content anyway. (For
+a user application implementation, one would need to handle data type
+values. This is a different story.)
+=== Expand ===
+To evaluate the input, press ''Expand''. The following result is
+returned.
+{{{
+  PossibleIndividual(s101)
+& Property(bar60)
+& ClassOfIndirectProperty(MaximumWorkingPressure)
+& exists u
+     (  (IndirectProperty(u) & hasPossessor(u, s101) & hasProperty(u, bar60))
+      & exists z
+           (  Classification(z)
+            & hasClassified(z, u)
+            & hasClassifier(z, MaximumWorkingPressure)))
+}}}
+During the expansion, the templates IndirectPropertyTriple and
+ClassificationTemplate, defined in Part 7, were expanded. The result
+makes perfectly good sense as an ISO 15926-2 pattern. The fact that
+the Expander applies the extension demonstrates that the syntactic
+structure is sound.
+
+We can easily see that the expanded results makes no reference to
+predicates not defined in ISO 15926-2. 
+=== Triples view of example ===
+If we wish to look at the result in a "triples" format, we can check
+the ''Skolemize result'' box before expansion. The result is as
+follows. 
+==== Prover9 format ====
+{{{
+  PossibleIndividual(s101)
+& Property(bar60)
+& ClassOfIndirectProperty(MaximumWorkingPressure)
+& (IndirectProperty(cu0) & hasPo.sessor(cu0, s101) & hasProperty(cu0, bar60))
+& Classification(cz0)
+& hasClassified(cz0, cu0)
+& hasClassifier(cz0, MaximumWorkingPressure)
+}}}
+With this, we have found a fully explicit expression, in terms of Part
+2 and individual terms, of the template statement. We have reduced a
+compact template statement to statements in the Part 2 language -- the
+basic language of ISO 15926.
+==== XML format ====
+A trivial search/replace macro can convert this into XML, for instance
+as follows.
+{{{
+<?xml version="1.0" encoding="UTF-8"?>
+<expandedtemplates>   
+  <node type="PossibleIndividual" name="s101"/>
+  <node type="Property" name="bar60"/>
+  <node type="ClassOfIndirectProperty" name="MaximumWorkingPressure"/>
+  <node type="IndirectProperty" name="cu0"/>
+  <edge type="hasPossessor" from="cu0" to="s101"/>
+  <edge type="hasProperty" from="cu0" to="bar60"/>
+  <node type="Classification" name="cz0"/>
+  <edge type="hasClassified" from="cz0" to="cu0"/>
+  <edge type="hasClassifier" from="cz0" to="MaximumWorkingPressure"/>
+</expandedtemplates> 
+}}}
+==== RDF format ====
+The following is a custom-made RDF representation that can be useful
+for visualization of the Part 2 structure of expanded template
+instances.
+{{{
+<?xml version="1.0" encoding="UTF-8"?>
+<rdf:RDF xmlns="http://test.org/Data#" xmlns:rdl="test.org/Data#"
+         xmlns:owl="http://www.w3.org/2002/07/owl#"
+         xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
+         xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#">
+   <rdl:PossibleIndividual rdf:about="s101"/>
+   <rdl:Property rdf:about="bar60"/>
+   <rdl:ClassOfIndirectProperty rdf:about="MaximumWorkingPressure"/>
+   <rdl:IndirectProperty rdf:about="cu0"/>
+   <rdf:Description rdf:about="cu0">
+      <rdl:hasPossessor rdf:resource="s101"/>
+   </rdf:Description>
+   <rdf:Description rdf:about="cu0">
+      <rdl:hasProperty rdf:resource="bar60"/>
+   </rdf:Description>
+   <rdf:Description rdf:about="cu0">
+      <rdf:type rdf:resource="MaximumWorkingPressure"/>
+   </rdf:Description>
+</rdf:RDF>
+}}}
+Visualized in [http://semweb.salzburgresearch.at/apps/rdf-gravity/ RDF-Gravity], this RDF file appears as follows.
+
+[[Image(PropertyOfIndividual-tpl-instances.png)]]
+== Option 2 ==
+=== Prepare axiom ===
+The template axiom is the following.
+{{{
+PropertyOfIndividual(x1, x2, x3, x4) <-> 
+  PossibleIndividual(x1) &
+  ArithmeticNumber(x2) &
+  Scale (x3) &
+  ClassOfIndirectProperty (x4) &
+  exists y1 exists y2 (MagnitudeOfProperty(y1, x2, x3) &
+    IndirectPropertyTriple(y2, x1, y1) &
+    ClassificationTemplate(y2,x4))
+}}}
+Notable corrections made vs. PDF version: 
+ - The fourth argument (x4) was missing
+ - "ArithmeticNumber" was misspelt as "ArithmaticNumber". This kind of
+   mistake can be tricky to spot in larger cases. As far as the
+   Expander is concerned, this introduces a new primitive concept
+   named "ArithmaticNumber".
+ - "Эy1, y2" needs rewriting as "exists y1 exists y2".
+ - Remember to add a final dot "." (very confusing in practice!)
+
+We replace the Option 1 formula in the Template Definitions frame by
+this one.
+=== Enter sample instance ===
+We need to enter the value "60" as an individual term that Prover9 can
+accept. I have written "d60" here.
+{{{
+PropertyOfIndividual(s101, d60, bar, MaximumWorkingPressure)
+}}}
+=== Expand ===
+The following result is returned.
+{{{
+  PossibleIndividual(s101)
+& ArithmeticNumber(d60)
+& Scale(bar)
+& ClassOfIndirectProperty(MaximumWorkingPressure)
+& exists y1
+     exists y2
+        (  (  Property(y1)
+            & ArithmeticNumber(d60)
+            & Scale(bar)
+            & exists u
+                 (  (  PropertyQuantification(u)
+                     & hasInput(u, y1)
+                     & hasResult(u, d60))
+                  & exists z
+                       (  Classification(z)
+                        & hasClassified(z, u)
+                        & hasClassifier(z, bar))))
+         & (IndirectProperty(y2) & hasPossessor(y2, s101) & hasProperty(y2, y1))
+         & exists z
+              (  Classification(z)
+               & hasClassified(z, y2)
+               & hasClassifier(z, MaximumWorkingPressure)))
+}}}
+This template applies MagnitudeOfProperty, one of the "Initial Set"
+templates of Part 7. Accordingly, the result is more complex. The
+difference is that the quantification of the property is here
+represented explicitly -- the property is explicitly stated to refer
+by way of the ''bar'' scale to the value 60.
+
+Once again, the successful expansion indicates that the template
+definition is sound. We can see by manual inspection that no reference
+is made to predicates not defined in Part 2. (But for the latter, we
+should really have a tool to make that check automatically. This
+shouldn't be difficult to write.)
+=== Triples view of example ===
+==== Prover9 format ====
+We select ''Skolemize result'' to produce the following.
+{{{
+  PossibleIndividual(s101)
+& ArithmeticNumber(d60)
+& Scale(bar)
+& ClassOfIndirectProperty(MaximumWorkingPressure)
+& (  Property(cy11)
+   & ArithmeticNumber(d60)
+   & Scale(bar)
+   & (PropertyQuantification(cu6) & hasInput(cu6, cy11) & hasResult(cu6, d60))
+   & Classification(cz8)
+   & hasClassified(cz8, cu6)
+   & hasClassifier(cz8, bar))
+& (IndirectProperty(cy21) & hasPossessor(cy21, s101) & hasProperty(cy21, cy11))
+& Classification(cz9)
+& hasClassified(cz9, cy21)
+& hasClassifier(cz9, MaximumWorkingPressure)
+}}}
+==== XML format ====
+Converted into XML, this can look as follows.
+{{{
+<?xml version="1.0" encoding="UTF-8"?>
+<expandedtemplates>   
+<node type="PossibleIndividual" name="s101"/>
+  <node type="ArithmeticNumber" name="d60"/>
+  <node type="Scale" name="bar"/>
+  <node type="ClassOfIndirectProperty" name="MaximumWorkingPressure"/>
+  <node type="Property" name="cy11"/>
+  <node type="ArithmeticNumber" name="d60"/>
+  <node type="Scale" name="bar"/>
+  <node type="PropertyQuantification" name="cu6"/>
+  <edge type="hasInput" from="cu6" to="cy11"/>
+  <edge type="hasResult" from="cu6" to="d60"/>
+  <node type="Classification" name="cz8"/>
+  <edge type="hasClassified" from="cz8" to="cu6"/>
+  <edge type="hasClassifier" from="cz8" to="bar"/>
+  <node type="IndirectProperty" name="cy21"/>
+  <edge type="hasPossessor" from="cy21" to="s101"/>
+  <edge type="hasProperty" from="cy21" to="cy11"/>
+  <node type="Classification" name="cz9"/>
+  <edge type="hasClassified" from="cz9" to="cy21"/>
+  <edge type="hasClassifier" from="cz9" to="MaximumWorkingPressure"/>
+</expandedtemplates>
+}}}
+==== RDF format ====
+The following is a custom-made RDF representation that can be useful
+for visualization of the Part 2 structure of expanded template
+instances.
+{{{
+<?xml version="1.0" encoding="UTF-8"?>
+<rdf:RDF xmlns="http://test.org/Data#" xmlns:rdl="test.org/Data#"
+         xmlns:owl="http://www.w3.org/2002/07/owl#"
+         xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
+         xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#">
+   <rdl:PossibleIndividual rdf:about="s101"/>
+   <rdl:ArithmeticNumber rdf:about="d60"/>
+   <rdl:Scale rdf:about="bar"/>
+   <rdl:ClassOfIndirectProperty rdf:about="MaximumWorkingPressure"/>
+   <rdl:Property rdf:about="cy11"/>
+   <rdl:ArithmeticNumber rdf:about="d60"/>
+   <rdl:Scale rdf:about="bar"/>
+   <rdl:PropertyQuantification rdf:about="cu6"/>
+   <rdl:IndirectProperty rdf:about="cy21"/>
+   <rdf:Description rdf:about="cu6">
+      <rdl:hasInput rdf:resource="cy11"/>
+   </rdf:Description>
+   <rdf:Description rdf:about="cu6">
+      <rdl:hasResult rdf:resource="d60"/>
+   </rdf:Description>
+   <rdf:Description rdf:about="cy21">
+      <rdl:hasPossessor rdf:resource="s101"/>
+   </rdf:Description>
+   <rdf:Description rdf:about="cy21">
+      <rdl:hasProperty rdf:resource="cy11"/>
+   </rdf:Description>
+   <rdf:Description rdf:about="cu6">
+      <rdf:type rdf:resource="bar"/>
+   </rdf:Description>
+   <rdf:Description rdf:about="cy21">
+      <rdf:type rdf:resource="MaximumWorkingPressure"/>
+   </rdf:Description>
+</rdf:RDF>
+}}}
+Visualized in [http://semweb.salzburgresearch.at/apps/rdf-gravity/ RDF-Gravity], this RDF file appears as follows.
+
+[[Image(PropertyOfIndividual2-tpl-instances.png)]]
+