POSC-Caesar FIATECH IDS-ADI Projects

Intelligent Data Sets Accelerating Deployment of ISO15926

Realizing Open Information Interoperability


Defining templates using ISO 15926-7 Template Expander and Prover9

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 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 Template Expander is a tool for working with template design. It was written in Java by Martin Giese. Development was funded by DNV IRM.

Java library

Using the Java library (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 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 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 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 RDF-Gravity, an RDF file can appear follows.

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 RDF-Gravity, this RDF file appears as follows.

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 RDF-Gravity, this RDF file appears as follows.


Attachments

Home
About PCA
Reference Data Services (RDS)
RDS Operations Support
Meetings and Conferences
ISO 15926
Special Interest Groups
Technical Advisory Board
Norwegian Continental Shelf Std
Projects
Search