= Verifying template rules using the Prover9 first-order reasoner =

''This page to be updated, to reflect current ISO 15926-7 TS draft.''

Preparation: Get hold of [http://www.cs.unm.edu/~mccune/prover9/ Prover9].

Back-link: SigMmt

== An example ==

This example stems from a need to have a typical kind of three-place templates (predicates) defined: The first two arguments should be filled by first and second roles of an ISO 15926 relationship (cf. [wiki:ISO15926inOWLPart2], [http://www.tc184-sc4.org/wg3ndocs/wg3n1328/lifecycle_integration_schema.html coRelationship]), the third by a class of which the pair is a member. In more common logical terminology, the triple will express that the pair of arguments one and two is a member of the relation given by the third argument.

With a relationship type ''E'', and the ''Classification'' type (or any other type one may wish to relate to the pair) abbreviated as ''C'', we wish to have a template with the following definition.

{{{
#!LatexEquation
ec(x,y,z) \leftrightarrow e(x,y) \wedge \forall u( eTriple(u,x,y) \rightarrow c(u,z) )
}}}
In Prover9 notation, the axiom looks like this:
{{{
ec(x,y,z) <-> e(x,y) & all u( eTriple(u,x,y) -> c(u,z) ) .
}}}

Using Prover9, we can show this somewhat complex axiom (complex in the sense that it contains a universally quantified conditional) is implied by the following set of very simple axioms.
{{{
% basic declarations for entity types E and C

eTriple(x,y,z) <-> E(x) & rE1(x,y) & rE2(x,z) .
eTriple(x,y,z) & eTriple(u,y,z) -> x=u .
e(x,y) <-> exists z( eTriple(z,x,y) ) .

cTriple(x,y,z) <-> C(x) & rC1(x,y) & rC2(x,z) .
cTriple(x,y,z) & cTriple(u,y,z) -> x=u .
c(x,y) <-> exists z( cTriple(z,x,y) ) .

% rules for ec (simple enough for SWRL)

ec(x,y,z) -> e(x,y) .
ec(x,y,z) & eTriple(u,x,y) -> c(u,z) .
eTriple(x,y,z) & c(x,u) -> ec(y,z,u) .
}}}