Changes between Version 1 and Version 2 of SigMmtTemplateAxioms
- Timestamp:
- 09/16/08 19:04:14 (16 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
SigMmtTemplateAxioms
v1 v2 11 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 12 13 {{{ 14 #!LatexEquation 15 ec(x,y,z) \leftrightarrow e(x,y) \wedge \forall u( eTriple(u,x,y) \rightarrow c(u,z) ) 16 }}} 17 In Prover9 notation, the axiom looks like this: 13 18 {{{ 14 19 ec(x,y,z) <-> e(x,y) & all u( eTriple(u,x,y) -> c(u,z) ) .