PGIP/Server/Examples.hs

	Examples.hs revision b5b5f5a2ebf5297bad207ef8f6621cdf441b75ed
dee396d567b71629f09f7e0692396afff732e33bChristian Maedermodule PGIP.Server.Examples where
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskidol :: String
dee396d567b71629f09f7e0692396afff732e33bChristian Maederdol = "%% a simple parthood ontology in OWL\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \logic OWL\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \ontology Parthood_OWL =\n\
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder      \  ObjectProperty: isPartOf\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \  ObjectProperty: isProperPartOf\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \  Characteristics: Asymmetric\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \  SubPropertyOf: isPartOf\n\
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski      \end\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \%% we cannot specify an object property to be both asymmetric and transitive in OWL. Therefore, we switch to Common Logic\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \logic CommonLogic\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \ontology Parthood_CL =\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder      \  Parthood_OWL\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder      \  with translation OWL22CommonLogic\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder      \then\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \  (forall (x y z) (if (and (isProperPartOf x y) (isProperPartOf y z))\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \                      (isProperPartOf x z)))\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \end"
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maedercasl :: String
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maedercasl = "spec Strict_Partial_Order =\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder       \sort Elem\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder       \pred __<__ : Elem * Elem\n\
6a9b85953df4e29a996536ffc7dbf7ef9dbc64c7Cui Jian       \forall x, y, z:Elem\n\
6a9b85953df4e29a996536ffc7dbf7ef9dbc64c7Cui Jian       \. not x < x %(irreflexive)%\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder       \. x < y /\\ y < z => x < z %(transitive)%\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder       \%% the following is logically entailed\n\
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder       \. x < y => not y < x %(asymmetric)% %implied\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder       \end"
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maederowl :: String
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maederowl = "Prefix: : <http://example.org/>\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder      \Ontology: <http://example.org/Family>\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \AnnotationProperty: Implied\n\
72ab63869f1e2ade586af4acb9218b46ab25ea9bCui Jian      \Class: Person\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder      \Class: Woman SubClassOf: Person\n\
74d9a385499bf903b24848dff450a153f525bda7Christian Maeder      \ObjectProperty: hasChild\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder      \Class: Mother \n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder       \      EquivalentTo: Woman and hasChild some Person\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \Individual: mary Types: Woman Facts: hasChild  john\n\
3bd08499449d7a250c1e297c59f52555d20c5dc2Cui Jian      \Individual: john Types: Person\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \Individual: mary \n\
72ab63869f1e2ade586af4acb9218b46ab25ea9bCui Jian      \     Types: Annotations: Implied \"true\"^^xsd:boolean\n\
72ab63869f1e2ade586af4acb9218b46ab25ea9bCui Jian      \            Mother"
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maederclif :: String
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maederclif = "(cl-text strict_partial_order.clif\n\
e389bfa263e2f58f594903f092731fb18f8a5392Christian Maeder       \  (forall (x) (not (< x x))) // irreflexive\n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder       \  (forall (x y z) (if (and (< x y) (< y z)) (< x z))) // transitive\n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder       \  (forall (x y) (if (< x y) (not (< y x)))) // asymmetric\n\
72ab63869f1e2ade586af4acb9218b46ab25ea9bCui Jian       \)"
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maederpropositional :: String
72ab63869f1e2ade586af4acb9218b46ab25ea9bCui Jianpropositional = "logic Propositional\n\
ef4bd99a054aac95f1bc9191e9972baa2d4e6faaChristian Maeder                \spec Raining =\n\
ef4bd99a054aac95f1bc9191e9972baa2d4e6faaChristian Maeder                \  props raining, wet_street\n\
ef4bd99a054aac95f1bc9191e9972baa2d4e6faaChristian Maeder                \  . raining => wet_street\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder                \                    %(if raining, the street is wet)%\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \end\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \spec Scenario1 = Raining then\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \  . not wet_street    %(the street is not wet)%\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \  . not raining       %(it is not raining)%  %implied\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \end\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \spec Scenario2 = Raining then\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \  . wet_street      %(the street is wet)%\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \  %% the following does not hold...\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \  . raining         %(hence it must rain...)%  %implied\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder                \end"
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maederrdf :: String
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maederrdf = "@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \@prefix dc: <http://purl.org/dc/elements/1.1/> .\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \@prefix ex: <http://example.org/stuff/1.0/> .\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder      \\n\
ef4bd99a054aac95f1bc9191e9972baa2d4e6faaChristian Maeder      \<http://www.w3.org/TR/rdf-syntax-grammar>\n\
ef4bd99a054aac95f1bc9191e9972baa2d4e6faaChristian Maeder      \  dc:title \"RDF/XML Syntax Specification (Revised)\" ;\n\
dee396d567b71629f09f7e0692396afff732e33bChristian Maeder      \  ex:editor [\n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder      \    ex:fullname \"Dave Beckett\";\n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder      \    ex:homePage <http://purl.org/net/dajobe/>\n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder      \  ] ."
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maedertptp :: String
72ab63869f1e2ade586af4acb9218b46ab25ea9bCui Jiantptp = "fof(irreflexive, axiom,\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder       \ ! [X]: (~ less(X, X))).\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder       \fof(transitive, axiom,\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder       \ ! [X, Y, Z]: ((less(X, Y) & less(Y, Z)) => less(X, Z))).\n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder       \fof(asYmmetric, conjecture,\n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder       \ ! [X, Y]: (less(X, Y) => ~ less(Y, X)))."
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maederhascasl :: String
72ab63869f1e2ade586af4acb9218b46ab25ea9bCui Jianhascasl = "logic HasCASL\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \spec Functions =\n\
0f54077ce2753086afc4025f6d282fd66a7a04adChristian Maeder          \  ops __o__ : forall a, b, c:Type . \n\
c614d41379feab88fe8298e068aa590420c4a018Christian Maeder          \               (b ->? c) * (a ->? b) -> (a ->? c);\n\
6a9b85953df4e29a996536ffc7dbf7ef9dbc64c7Cui Jian          \      id    : forall a:Type . a ->? a;\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \  vars a, b, c : Type;\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \         g         : b ->? c;\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \         f         : a ->? b;\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \         x         : a\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \   . g o f = \\ x . g (f x)               %(o_def)%\n\
6a9b85953df4e29a996536ffc7dbf7ef9dbc64c7Cui Jian          \   . id = \\ x . x                        %(id_def)%\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \ then %implies\n\
6a9b85953df4e29a996536ffc7dbf7ef9dbc64c7Cui Jian          \  vars a, b, c , d : Type;\n\
b91b82fd2625c349da6284f252cf4c50a6519650Christian Maeder          \         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"