Version 3 (modified by jowik, 16 years ago)

--

Verifying template rules using the Prover9 first-order reasoner

This page is just a rough draft, but the example case works, so it makes sense to make it available here so people can experiment.

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

The good news is, these simple axioms can be expressed in SWRL (i.e., at least if we allow ourselves the use of the Protégé swrlx extension implemented for the Protégé SWRLTab, makeOWLThing).

Home
About PCA
Reference Data Services
Projects
Workgroups