msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

definitions for some high-order predicates that were missing

Browse Source
This commit is contained in:
krasimir
2010-06-06 12:10:49 +00:00
parent db3eb23d5f
commit 1371f630b6
1 changed files with 17 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
examples/SUMO/Merge.gf
View File

@@ -5780,6 +5780,9 @@ abstract Merge = Basic ** {
-- only if the relation is reflexive on the set or class, -- only if the relation is reflexive on the set or class,
-- and it is both an antisymmetric relation, and a transitive relation. -- and it is both an antisymmetric relation, and a transitive relation.
fun partialOrderingOn : (c : Class) -> (El c -> El c -> Formula) -> Formula ; 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 -- The basic mereological relation. All other
-- mereological relations are defined in terms of this one. -- 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 -- A binary predicate is reflexive on a set or class only if
-- every instance of the set or class bears the relation to itself. -- every instance of the set or class bears the relation to itself.
fun reflexiveOn : (c : Class) -> (El c -> El c -> Formula) -> Formula ; 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 -- (relatedEvent ?EVENT1 ?EVENT2) means
-- that the Process ?EVENT1 is related to the Process ?EVENT2. The -- 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 time : El Physical -> El TimePosition -> Formula ;
fun totalOrderingOn : (c : Class) -> (El c -> El c -> Formula) -> 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 -- (top ?TOP ?OBJECT) means that ?TOP is the highest maximal
-- superficial part of ?OBJECT. -- superficial part of ?OBJECT.
@@ -6189,6 +6195,17 @@ abstract Merge = Basic ** {
-- penetrates are subrelations of traverses. -- penetrates are subrelations of traverses.
fun traverses : El Object -> El Object -> Formula ; 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 -- The BinaryPredicate that relates a Sentence
-- to its TruthValue. -- to its TruthValue.
fun truth : El Sentence -> El TruthValue -> Formula ; fun truth : El Sentence -> El TruthValue -> Formula ;