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 Prover9.
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. ISO15926inOWLPart2, 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.
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) .