diff options
| author | bjorn <bjorn@bringert.net> | 2008-08-14 07:58:04 +0000 |
|---|---|---|
| committer | bjorn <bjorn@bringert.net> | 2008-08-14 07:58:04 +0000 |
| commit | 77270a010a0b453e9a84c3e62db7cfd22e49d55d (patch) | |
| tree | d17682a545d6ac1e68ff49b8c20964182794baf7 /grammars/logic/LogicEng.gf | |
| parent | 0bbb906141711767678f82b15a7b43e65e0b5bd6 (diff) | |
Remove the grammars directory. It was full of old grammars that don't compile these days. See the old source distributions if you want them.
Diffstat (limited to 'grammars/logic/LogicEng.gf')
| -rw-r--r-- | grammars/logic/LogicEng.gf | 60 |
1 files changed, 0 insertions, 60 deletions
diff --git a/grammars/logic/LogicEng.gf b/grammars/logic/LogicEng.gf deleted file mode 100644 index b708068e2..000000000 --- a/grammars/logic/LogicEng.gf +++ /dev/null @@ -1,60 +0,0 @@ -concrete LogicEng of Logic = open LogicResEng, Prelude in { - -flags lexer=vars ; unlexer=text ; - -lincat - Dom = {s : Num => Str} ; - Prop, Elem = {s : Str} ; - -lin -Statement A = {s = A.s ++ "."} ; -ThmWithProof A a = {s = - ["Theorem ."] ++ A.s ++ "." ++ PARA ++ "Proof" ++ "." ++ a.s ++ "."} ; -ThmWithTrivialProof A a = - {s = "Theorem" ++ "." ++ A.s ++ "." ++ PARA ++ "Proof" ++ "." ++ "Trivial" ++ "."} ; -Disj A B = {s = A.s ++ "or" ++ B.s} ; -Conj A B = {s = A.s ++ "and" ++ B.s} ; -Impl A B = {s = "if" ++ A.s ++ "then" ++ B.s} ; -Univ A B = {s = ["for all"] ++ A.s ! pl ++ B.$0 ++ "," ++ B.s} ; -Exist A B = - {s = ["there exists"] ++ indef ++ A.s ! sg ++ B.$0 ++ ["such that"] ++ B.s} ; -Abs = {s = ["we have a contradiction"]} ; -Neg A = {s = ["it is not the case that"] ++ A.s} ; -ImplP A B = {s = "if" ++ A.s ++ "then" ++ B.s} ; -ConjI A B a b = {s = a.s ++ "." ++ b.s ++ [". Hence"] ++ A.s ++ "and" ++ B.s} ; -ConjEl A B c = {s = c.s ++ [". A fortiori ,"] ++ A.s} ; -ConjEr A B c = {s = c.s ++ [". A fortiori ,"] ++ B.s} ; -DisjIl A B a = {s = a.s ++ [". A fortiori ,"] ++ A.s ++ "or" ++ B.s} ; -DisjIr A B b = {s = b.s ++ [". A fortiori ,"] ++ A.s ++ "or" ++ B.s} ; -DisjE A B C c d e = {s = - c.s ++ - [". There are two possibilities . First , assume"] ++ - A.s ++ "(" ++ d.$0 ++ ")" ++ "." ++ d.s ++ - [". Second , assume"] ++ B.s ++ "(" ++ e.$0 ++ ")" ++ "." ++ e.s ++ - [". Thus"] ++ C.s ++ ["in both cases"]} ; -ImplI A B b = {s = - "assume" ++ A.s ++ "(" ++ b.$0 ++ ")" ++ "." ++ - b.s ++ [". Hence , if"] ++ A.s ++ "then" ++ B.s} ; -ImplE A B c a = {s = a.s ++ [". But"] ++ c.s ++ [". Hence"] ++ B.s} ; -NegI A b = {s = - "assume" ++ A.s ++ "(" ++ b.$0 ++ ")" ++ "." ++ b.s ++ - [". Hence, it is not the case that"] ++ A.s} ; -NegE A c a = - {s = a.s ++ [". But"] ++ c.s ++ [". We have a contradiction"]} ; -UnivI A B b = {s = - ["consider an arbitrary"] ++ A.s ! sg ++ b.$0 ++ "." ++ b.s ++ - [". Hence, for all"] ++ A.s ! pl ++ B.$0 ++ "," ++ B.s} ; -UnivE A B c a = - {s = c.s ++ [". Hence"] ++ B.s ++ "for" ++ B.$0 ++ ["set to"] ++ a.s} ; -ExistI A B a b = {s = - b.s ++ [". Hence, there exists"] ++ indef ++ - A.s ! sg ++ B.$0 ++ ["such that"] ++ B.s} ; -ExistE A B C c d = {s = - c.s ++ [". Consider an arbitrary"] ++ d.$0 ++ - ["and assume that"] ++ B.s ++ "(" ++ d.$1 ++ ")" ++ "." ++ d.s ++ - [". Hence"] ++ C.s ++ ["independently of"] ++ d.$0} ; -AbsE C c = {s = c.s ++ [". We may conclude"] ++ C.s} ; -Hypo A a = {s = ["by the hypothesis"] ++ a.s ++ "," ++ A.s} ; -Pron _ _ = {s = "it"} ; - -} ; |
