| | 1 | = Verifying template rules using the Prover9 first-order reasoner = |
| | 2 | |
| | 3 | ''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.'' |
| | 4 | |
| | 5 | Preparation: Get hold of [http://www.cs.unm.edu/~mccune/prover9/ Prover9]. |
| | 6 | |
| | 7 | == An example == |
| | 8 | |
| | 9 | 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. |
| | 10 | |
| | 11 | 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. |
| | 12 | |
| | 13 | {{{ |
| | 14 | ec(x,y,z) <-> e(x,y) & all u( eTriple(u,x,y) -> c(u,z) ) . |
| | 15 | }}} |
| | 16 | |
| | 17 | 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. |
| | 18 | {{{ |
| | 19 | % basic declarations for entity types E and C |
| | 20 | |
| | 21 | eTriple(x,y,z) <-> E(x) & rE1(x,y) & rE2(x,z) . |
| | 22 | eTriple(x,y,z) & eTriple(u,y,z) -> x=u . |
| | 23 | e(x,y) <-> exists z( eTriple(z,x,y) ) . |
| | 24 | |
| | 25 | cTriple(x,y,z) <-> C(x) & rC1(x,y) & rC2(x,z) . |
| | 26 | cTriple(x,y,z) & cTriple(u,y,z) -> x=u . |
| | 27 | c(x,y) <-> exists z( cTriple(z,x,y) ) . |
| | 28 | |
| | 29 | % rules for ec (simple enough for SWRL) |
| | 30 | |
| | 31 | ec(x,y,z) -> e(x,y) . |
| | 32 | ec(x,y,z) & eTriple(u,x,y) -> c(u,z) . |
| | 33 | eTriple(x,y,z) & c(x,u) -> ec(y,z,u) . |
| | 34 | }}} |
| | 35 | 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é [http://protege.cim3.net/cgi-bin/wiki.pl?SWRLExtensionsBuiltIns swrlx] extension implemented for the Protégé SWRLTab, `makeOWLThing`). |
