module PGIP.Server.Examples where
dol :: String
dol = "%% a simple parthood ontology in OWL\n\
\logic OWL\n\
\ontology Parthood_OWL =\n\
\ ObjectProperty: isPartOf\n\
\ ObjectProperty: isProperPartOf\n\
\ Characteristics: Asymmetric\n\
\ SubPropertyOf: isPartOf\n\
\end\n\
\\n\
\%% we cannot specify an object property to be both asymmetric and transitive in OWL. Therefore, we switch to Common Logic\n\
\logic CommonLogic\n\
\ontology Parthood_CL =\n\
\ Parthood_OWL\n\
\ with translation OWL22CommonLogic\n\
\then\n\
\ (forall (x y z) (if (and (isProperPartOf x y) (isProperPartOf y z))\n\
\ (isProperPartOf x z)))\n\
\end"
casl :: String
casl = "spec Strict_Partial_Order =\n\
\sort Elem\n\
\pred __<__ : Elem * Elem\n\
\forall x, y, z:Elem\n\
\. not x < x %(irreflexive)%\n\
\. x < y /\\ y < z => x < z %(transitive)%\n\
\%% the following is logically entailed\n\
\. x < y => not y < x %(asymmetric)% %implied\n\
\end"
owl :: String
owl = "Prefix: : <http://example.org/>\n\
\Ontology: <http://example.org/Family>\n\
\AnnotationProperty: Implied\n\
\Class: Person\n\
\Class: Woman SubClassOf: Person\n\
\ObjectProperty: hasChild\n\
\Class: Mother \n\
\ EquivalentTo: Woman and hasChild some Person\n\
\Individual: mary Types: Woman Facts: hasChild john\n\
\Individual: john Types: Person\n\
\Individual: mary \n\
\ Types: Annotations: Implied \"true\"^^xsd:boolean\n\
\ Mother"
clif :: String
clif = "(cl-text strict_partial_order.clif\n\
\ (forall (x) (not (< x x))) // irreflexive\n\
\ (forall (x y z) (if (and (< x y) (< y z)) (< x z))) // transitive\n\
\ (forall (x y) (if (< x y) (not (< y x)))) // asymmetric\n\
\)"
propositional :: String
propositional = "logic Propositional\n\
\spec Raining =\n\
\ props raining, wet_street\n\
\ . raining => wet_street\n\
\ %(if raining, the street is wet)%\n\
\end\n\
\spec Scenario1 = Raining then\n\
\ . not wet_street %(the street is not wet)%\n\
\ . not raining %(it is not raining)% %implied\n\
\end\n\
\spec Scenario2 = Raining then\n\
\ . wet_street %(the street is wet)%\n\
\ %% the following does not hold...\n\
\ . raining %(hence it must rain...)% %implied\n\
\end"
rdf :: String
rdf = "@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .\n\
\@prefix dc: <http://purl.org/dc/elements/1.1/> .\n\
\@prefix ex: <http://example.org/stuff/1.0/> .\n\
\\n\
\ dc:title \"RDF/XML Syntax Specification (Revised)\" ;\n\
\ ex:editor [\n\
\ ex:fullname \"Dave Beckett\";\n\
\ ex:homePage <http://purl.org/net/dajobe/>\n\
\ ] ."
tptp :: String
tptp = "fof(irreflexive, axiom,\n\
\ ! [X]: (~ less(X, X))).\n\
\fof(transitive, axiom,\n\
\ ! [X, Y, Z]: ((less(X, Y) & less(Y, Z)) => less(X, Z))).\n\
\fof(asYmmetric, conjecture,\n\
\ ! [X, Y]: (less(X, Y) => ~ less(Y, X)))."
hascasl :: String
hascasl = "logic HasCASL\n\
\spec Functions =\n\
\ ops __o__ : forall a, b, c:Type . \n\
\ (b ->? c) * (a ->? b) -> (a ->? c);\n\
\ id : forall a:Type . a ->? a;\n\
\ vars a, b, c : Type;\n\
\ g : b ->? c;\n\
\ f : a ->? b;\n\
\ x : a\n\
\ . g o f = \\ x . g (f x) %(o_def)%\n\
\ . id = \\ x . x %(id_def)%\n\
\ then %implies\n\
\ vars a, b, c , d : Type;\n\
\ f' : a ->? a;\n\
\ h : c ->? d;\n\
\ g : b ->? c;\n\
\ f : a ->? b\n\
\ . h o (g o f) = (h o g) o f %(o_assoc)%\n\
\ . f' o id = f' %(id_neut)%\n\
\ . f' o f' = id => forall x, y:a .\n\
\ f' x = f' y => x = y %(inj)%\n\
\ . f' o f' = id => forall x:a .\n\
\ exists y:a . f' y = x %(surj)%\n\
\end"
modal :: String
modal = "logic Modal\n\
\spec M =\n\
\ modality empty { [](p /\\ q) => []p }\n\
\end\n\
\spec K =\n\
\ modality empty { [] true; [](p => q) => ([]p => []q) }\n\
\end\n\
\spec T = K then\n\
\ modality empty { []p => p }\n\
\end\n\
\spec S4 = T then\n\
\ modality empty { []A => [][]A }\n\
\end\n\
\spec S5 = T then\n\
\ modality empty {<>A => []<>A}\n\
\end"