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.

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