{{{
#!comment
NB! Make sure that you follow the guidelines: http://trac.posccaesar.org/wiki/IdsAdiEditing
}}}
[[TracNav(TracNav/IdsAdi)]]
[[Image(wiki:IdsAdiBranding:Logo-128x128.gif)]]
= 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
[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.
{{{
}}}
==== 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.
{{{
}}}
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.
{{{
}}}
==== 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.
{{{
}}}
Visualized in [http://semweb.salzburgresearch.at/apps/rdf-gravity/ RDF-Gravity], this RDF file appears as follows.
[[Image(PropertyOfIndividual2-tpl-instances.png)]]
----