From 455d9558417a759fae3ccbe5cde5c9f5064a08d2 Mon Sep 17 00:00:00 2001 From: krasimir Date: Sun, 6 Jun 2010 11:06:44 +0000 Subject: changes in SUMO: formatting and fixes for lots of lots of small problems --- examples/SUMO/HigherOrder.gf | 98 -------------------------------------------- 1 file changed, 98 deletions(-) delete mode 100644 examples/SUMO/HigherOrder.gf (limited to 'examples/SUMO/HigherOrder.gf') diff --git a/examples/SUMO/HigherOrder.gf b/examples/SUMO/HigherOrder.gf deleted file mode 100644 index fef66885e..000000000 --- a/examples/SUMO/HigherOrder.gf +++ /dev/null @@ -1,98 +0,0 @@ ---# -path=.:englishExtended -abstract HigherOrder = Merge ** { - -fun SingleValuedRelation : (c : Class) -> (El c -> Formula) -> Formula; -def SingleValuedRelation c f = forall c (\x -> forall c (\y -> impl (and (f (var c c ? x)) (f (var c c ? y))) (equal (var c Entity ? x) (var c Entity ? y)))); - -fun AntisymmetricRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def AntisymmetricRelation c f = forall c (\x -> forall c (\y -> impl (and (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? x))) (equal (var c Entity ? x) (var c Entity ? y)))); - -fun IntentionalRelation : (c1,c2 : Class) -> (El c1 -> El c2 -> Formula) -> Formula ; -def IntentionalRelation c1 c2 f = forall c1 (\x -> forall c2 (\y -> inScopeOfInterest (var c1 CognitiveAgent ? x) (var c2 Entity ? y))); --- assume binary predicate, since it is mostly used for that - -fun ReflexiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def ReflexiveRelation c f = forall c (\x -> f (var c c ? x) (var c c ? x)); - -fun SymmetricRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def SymmetricRelation c f = forall c (\x -> forall c(\y -> impl (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? x)))); - -fun EquivalenceRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def EquivalenceRelation c f = and (and (ReflexiveRelation c f) (SymmetricRelation c f)) (TransitiveRelation c f); - -fun TransitiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def TransitiveRelation c f = forall c (\x -> forall c (\y -> forall c(\z -> impl (and (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? z))) (f (var c c ? x) (var c c ? z))))); - -fun IrreflexiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def IrreflexiveRelation c f = forall c (\x -> not (f (var c c ? x) (var c c ? x))); - -fun AsymmetricRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def AsymmetricRelation c f = and (AntisymmetricRelation c f) (IrreflexiveRelation c f); - -fun PropositionalAttitude : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def PropositionalAttitude c f = (AsymmetricRelation c f); - -fun ObjectAttitude : (c1,c2 : Class) -> (El c1 -> El c2 -> Formula) -> Formula ; -def ObjectAttitude c1 c2 f = IntentionalRelation c1 c2 f ; - -fun IntransitiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def IntransitiveRelation c f = forall c (\x -> forall c (\y -> forall c(\z -> impl (and (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? z))) (not (f (var c c ? x) (var c c ? z)))))); - -fun PartialOrderingRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def PartialOrderingRelation c f = and (and (TransitiveRelation c f) (AntisymmetricRelation c f)) (ReflexiveRelation c f); - -fun TrichotomizingRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def TrichotomizingRelation c f = forall c (\x -> forall c (\y -> -or -(or -(and -(and (f (var c c ? x) (var c c ? y)) -(not (equal (var c Entity ? x) (var c Entity ? y)))) -(not (f (var c c ? y) (var c c ? x)))) -(and -(and (not (f (var c c ? x) (var c c ? y))) -(equal (var c Entity ? x) (var c Entity ? y))) -(not (f (var c c ? y) (var c c ? x))))) -(and -(and (f (var c c ? y) (var c c ? x)) -(not (equal (var c Entity ? x) (var c Entity ? y)))) -(not (f (var c c ? x) (var c c ? y)))))); - -fun TotalOrderingRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ; -def TotalOrderingRelation c f = and (PartialOrderingRelation c f) (TrichotomizingRelation c f) ; - -fun OneToOneFunction : (c1, c2 : Class) -> (El c1 -> Ind c2) -> Formula ; -def OneToOneFunction c1 c2 f = forall c1(\x -> - forall c1(\y -> impl (not(equal (var c1 Entity ? x) (var c1 Entity ? y))) (not (equal (el c2 Entity ? (f (var c1 c1 ? x))) (el c2 Entity ? (f (var c1 c1 ? y))))))); - -fun SequenceFunction : (c : Class) -> (El Integer -> Ind c) -> Formula ; -def SequenceFunction c f = OneToOneFunction Integer c f ; - -fun AssociativeFunction : (c : Class) -> (El c -> El c -> Ind c) -> Formula ; -def AssociativeFunction c f = forall c(\x -> - forall c(\y -> - forall c(\z -> equal (el c Entity ? (f (var c c ? x) (el c c ? (f (var c c ? y) (var c c ? z))))) (el c Entity ? (f (el c c ? (f (var c c ? x) (var c c ? y))) (var c c ? z)))))); - -fun CommutativeFunction : (c1,c2 : Class) -> (El c1 -> El c1 -> Ind c2) -> Formula ; -def CommutativeFunction c1 c2 f = forall c1 (\x -> - forall c1 (\y -> - equal (el c2 Entity ? (f (var c1 c1 ? x) (var c1 c1 ? y))) (el c2 Entity ? (f (var c1 c1 ? y) (var c1 c1 ? y))))); - -fun identityElement : (c : Class) -> (El c -> El c -> Ind c) -> El c -> Formula ; -def identityElement c f elem = forall c(\x -> equal (el c Entity ? (f (var c c ? x) elem)) (var c Entity ? x)); - -fun distributes : (c : Class) -> (El c -> El c -> Ind c) -> (El c -> El c -> Ind c) -> Formula ; -def distributes c f g = forall c (\x -> forall c (\y -> forall c (\z -> equal (el c Entity ? (g (el c c ? (f (var c c ? x) (var c c ? y))) (var c c ? z))) (el c Entity ? (f (el c c ? (g (var c c ? x) (var c c ? z))) (el c c ? (g (var c c ? y) (var c c ? z)))))))); - -fun inverse : (c : Class) -> (El c -> El c -> Formula) -> (El c -> El c -> Formula) -> Formula ; -def inverse c f g = forall c (\x -> forall c (\y -> equiv (f (var c c ? x) (var c c ? y)) (g (var c c ? y) (var c c ? x)))); - -fun subRelation2El : (c1,c2,c3,c4 : Class) -> (El c1 -> El c2 -> Formula) -> (El c3 -> El c4 -> Formula) -> Formula ; -def subRelation2El c1 c2 c3 c4 f g = forall c1 (\x -> forall c2 (\y -> impl (f (var c1 c1 ? x) (var c2 c2 ? y)) (g (var c1 c3 ? x) (var c2 c4 ? y)))); - -fun KappaFn : (c : Class) -> (Ind c -> Formula) -> Class ; - - - - -}; \ No newline at end of file -- cgit v1.2.3