= 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) . }}}