diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/SUMO/Merge.gf | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/examples/SUMO/Merge.gf b/examples/SUMO/Merge.gf index 297c2e0f8..bbfec29dd 100644 --- a/examples/SUMO/Merge.gf +++ b/examples/SUMO/Merge.gf @@ -5780,6 +5780,9 @@ abstract Merge = Basic ** { -- only if the relation is reflexive on the set or class,
-- and it is both an antisymmetric relation, and a transitive relation.
fun partialOrderingOn : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
+ def partialOrderingOn c p = and (reflexiveOn c p)
+ (and (TransitiveRelation c p)
+ (AntisymmetricRelation c p)) ;
-- The basic mereological relation. All other
-- mereological relations are defined in terms of this one.
@@ -5927,6 +5930,7 @@ abstract Merge = Basic ** { -- A binary predicate is reflexive on a set or class only if
-- every instance of the set or class bears the relation to itself.
fun reflexiveOn : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
+ def reflexiveOn c p = forall c (\INST -> p (var c c ? INST) (var c c ? INST)) ;
-- (relatedEvent ?EVENT1 ?EVENT2) means
-- that the Process ?EVENT1 is related to the Process ?EVENT2. The
@@ -6174,6 +6178,8 @@ abstract Merge = Basic ** { fun time : El Physical -> El TimePosition -> Formula ;
fun totalOrderingOn : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
+ def totalOrderingOn c p = and (partialOrderingOn c p)
+ (trichotomizingOn c p) ;
-- (top ?TOP ?OBJECT) means that ?TOP is the highest maximal
-- superficial part of ?OBJECT.
@@ -6189,6 +6195,17 @@ abstract Merge = Basic ** { -- penetrates are subrelations of traverses.
fun traverses : El Object -> El Object -> Formula ;
+ -- A binary predicate ?REL is trichotomizing on a set or class only if,
+ -- for all instances ?INST1 and ?INST2 of the set or class,
+ -- at least one of the following holds:
+ -- (?REL ?INST1 ?INST2),
+ -- (?REL ?INST2 ?INST1) or
+ -- (equal ?INST1 ?INST2)
+ fun trichotomizingOn : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
+ def trichotomizingOn c p = forall c (\INST1 -> forall c (\INST2 -> or (or (p (var c c ? INST1) (var c c ? INST2))
+ (p (var c c ? INST2) (var c c ? INST1)))
+ (equal (var c Entity ? INST1) (var c Entity ? INST2)))) ;
+
-- The BinaryPredicate that relates a Sentence
-- to its TruthValue.
fun truth : El Sentence -> El TruthValue -> Formula ;
|