{{{ #!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)]] ----