Founding the newly structured GF2.0 cvs archive.

grammars/logic/Arithm.gf

@@ -0,0 +1,63 @@
+abstract Arithm = Logic ** {
+
+-- arithmetic
+fun 
+  Nat, Real  : Dom ;
+  zero : Elem Nat ;
+  succ : Elem Nat -> Elem Nat ;
+  
+  trunc : Elem Real -> Elem Nat ;
+
+  EqNat : (m,n : Elem Nat) -> Prop ;
+  LtNat : (m,n : Elem Nat) -> Prop ;
+  Div   : (m,n : Elem Nat) -> Prop ;
+  Even  : Elem Nat -> Prop ;
+  Odd   : Elem Nat -> Prop ;
+  Prime : Elem Nat -> Prop ;
+
+  one  : Elem Nat ;
+  two  : Elem Nat ;
+  sum  : (m,n : Elem Nat) -> Elem Nat ;
+  prod : (m,n : Elem Nat) -> Elem Nat ;
+
+  evax1 : Proof (Even zero) ;
+  evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (succ n)) ;
+  evax3 : (n : Elem Nat) -> Proof (Odd n)  -> Proof (Even (succ n)) ;
+  eqax1 : Proof (EqNat zero zero) ;
+  eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> Proof (EqNat (succ m) (succ n)) ;
+
+  IndNat : (C : Elem Nat -> Prop) -> 
+             Proof (C zero) -> 
+             ((x : Elem Nat) -> Proof (C x) -> Proof (C (succ x))) -> 
+                Proof (Univ Nat C) ;
+
+def 
+  one = succ zero ;
+  two = succ one ;
+  sum m zero = m ;
+  sum m (succ n) = succ (sum m n) ;
+  prod m zero = zero ;
+  prod m (succ n) = sum (prod m n) m ;
+  LtNat m n = Exist Nat (\x -> EqNat n (sum m (succ x))) ;
+  Div m n = Exist Nat (\x -> EqNat m (prod x n)) ;
+  Prime n = Conj 
+              (LtNat one n) 
+              (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
+
+fun ex1 : Text ;
+def ex1 = 
+  ThmWithProof 
+    (Univ Nat (\x -> Disj (Even x) (Odd x))) 
+    (IndNat 
+       (\x -> Disj (Even x) (Odd x)) 
+       (DisjIl (Even zero) (Odd zero) evax1) 
+       (\x -> \h -> DisjE (Even x) (Odd x) (Disj (Even (succ x)) (Odd (succ x))) 
+         (Hypo (Disj (Even x) (Odd x)) h) 
+         (\a -> DisjIr (Even (succ x)) (Odd (succ x)) 
+            (evax2 x (Hypo (Even x) a))) 
+         (\b -> DisjIl (Even (succ x)) (Odd (succ x)) 
+            (evax3 x (Hypo (Odd x) b))
+         )
+       )
+     ) ;
+} ;

grammars/logic/ArithmEng.gf

@@ -0,0 +1,40 @@
+concrete ArithmEng of Arithm = LogicEng ** open LogicResEng in {
+
+lin
+  Nat = {s = nomReg "number"} ;
+  zero = ss "zero" ;
+  succ = fun1 "successor" ;
+
+  EqNat = adj2 ["equal to"] ;
+  LtNat = adj2 ["smaller than"] ;
+  Div   = adj2 ["divisible by"] ;
+  Even  = adj1 "even" ;
+  Odd   = adj1 "odd" ;
+  Prime = adj1 "prime" ;
+
+  one = ss "one" ;
+  two = ss "two" ;
+  sum = fun2 "sum" ;
+  prod = fun2 "product" ;
+
+  evax1 = ss ["by the first axiom of evenness , zero is even"] ;
+  evax2 n c = {s = 
+    c.s ++ [". By the second axiom of evenness , the successor of"] ++ 
+    n.s ++ ["is odd"]} ;
+  evax3 n c = {s = 
+    c.s ++ [". By the third axiom of evenness , the successor of"] ++ 
+    n.s ++ ["is even"]} ;
+  eqax1 = ss ["by the first axiom of equality , zero is equal to zero"] ;
+  eqax2 m n c = {s = 
+    c.s ++ [". By the second axiom of equality , the successor of"] ++ m.s ++ 
+    ["is equal to the successor of"] ++ n.s} ;
+  IndNat C d e = {s = 
+    ["we proceed by induction . For the basis ,"] ++ d.s ++ 
+    [". For the induction step, consider a number"] ++ C.$0 ++ 
+    ["and assume"] ++ C.s ++ "(" ++ e.$1 ++ ")" ++ "." ++ e.s ++ 
+    ["Hence, for all numbers"] ++ C.$0 ++ "," ++ C.s} ;
+
+  ex1 = ss ["The first theorem and its proof ."] ;
+
+} ;
+

grammars/logic/Logic.gf

@@ -0,0 +1,82 @@
+-- many-sorted predicate calculus
+-- AR 1999, revised 2001
+
+abstract Logic = {
+
+flags startcat=Prop ; -- this is what you want to parse
+
+cat 
+  Prop ;       -- proposition
+  Dom ;        -- domain of quantification
+  Elem Dom ;   -- individual element of a domain
+  Proof Prop ; -- proof of a proposition
+  Text ;       -- theorem with proof etc. 
+
+fun 
+  -- texts
+  Statement : Prop -> Text ;
+  ThmWithProof : (A : Prop) -> Proof A -> Text ;
+  ThmWithTrivialProof : (A : Prop) -> Proof A -> Text ;
+
+  -- logically complex propositions
+  Disj : (A,B : Prop) -> Prop ;
+  Conj : (A,B : Prop) -> Prop ;
+  Impl : (A,B : Prop) -> Prop ;
+  Abs  : Prop ;
+  Neg  : Prop -> Prop ;
+
+  Univ  : (A : Dom) -> (Elem A -> Prop) -> Prop ;
+  Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
+
+  -- progressive implication ŕ la type theory
+  ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
+
+  -- inference rules
+  ConjI  : (A,B : Prop) -> Proof A -> Proof B -> Proof (Conj A B) ;
+  ConjEl : (A,B : Prop) -> Proof (Conj A B) -> Proof A ;
+  ConjEr : (A,B : Prop) -> Proof (Conj A B) -> Proof B ;
+  DisjIl : (A,B : Prop) -> Proof A -> Proof (Disj A B) ;
+  DisjIr : (A,B : Prop) -> Proof B -> Proof (Disj A B) ;
+  DisjE  : (A,B,C : Prop) -> Proof (Disj A B) -> 
+              (Proof A -> Proof C) -> (Proof B -> Proof C) -> Proof C ;
+  ImplI  : (A,B : Prop) -> (Proof A -> Proof B) -> Proof (Impl A B) ;
+  ImplE  : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
+  NegI   : (A : Prop) -> (Proof A -> Proof Abs) -> Proof (Neg A) ;
+  NegE   : (A : Prop) -> Proof (Neg A) -> Proof A -> Proof Abs ;
+  AbsE   : (C : Prop) -> Proof Abs -> Proof C ;
+
+  UnivI  : (A : Dom) -> (B : Elem A -> Prop) -> 
+              ((x : Elem A) -> Proof (B x)) -> Proof (Univ A B) ;
+  UnivE  : (A : Dom) -> (B : Elem A -> Prop) -> 
+              Proof (Univ A B) -> (a : Elem A) -> Proof (B a) ;
+  ExistI : (A : Dom) -> (B : Elem A -> Prop) -> 
+              (a : Elem A) -> Proof (B a) -> Proof (Exist A B) ;
+  ExistE : (A : Dom) -> (B : Elem A -> Prop) -> (C : Prop) -> 
+              Proof (Exist A B) -> ((x : Elem A) -> Proof (B x) -> Proof C) -> 
+              Proof C ;
+
+  -- use a hypothesis
+  Hypo : (A : Prop) -> Proof A -> Proof A ;
+
+  -- pronoun
+  Pron : (A : Dom) -> Elem A -> Elem A ;
+
+data
+  Proof = ConjI | DisjIl | DisjIr ;
+
+def 
+  -- proof normalization
+  ConjEl _ _ (ConjI _ _ a _) = a ;
+  ConjEr _ _ (ConjI _ _ _ b) = b ;
+  DisjE _ _ _ (DisjIl _ _ a) d _ = d a ;
+  DisjE _ _ _ (DisjIr _ _ b) _ e = e b ;
+  ImplE _ _ (ImplI _ _ b) a = b a ;
+  NegE _ (NegI _ b) a = b a ;
+  UnivE _ _ (UnivI _ _ b) a = b a ;
+  ExistE _ _ _ (ExistI _ _ a b) d = d a b ;
+
+  -- Hypo and Pron are identities
+  Hypo _ a = a ;
+  Pron _ a = a ;
+
+} ;

grammars/logic/LogicEng.gf

@@ -0,0 +1,59 @@
+concrete LogicEng of Logic = open LogicResEng 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 ++ [". <p> Proof ."] ++ a.s ++ "."} ;
+ThmWithTrivialProof A a = 
+  {s = "Theorem" ++ "." ++ A.s ++ [". <p> 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"} ;
+
+} ;

grammars/logic/LogicResEng.gf

@@ -0,0 +1,27 @@
+resource LogicResEng = {
+
+param Num = sg | pl  ;
+
+oper 
+  
+  ss  : Str -> {s : Str} = \s -> {s = s} ;
+
+  nomReg : Str -> Num => Str = \s -> table {sg => s ; pl => s + "s"} ;
+
+  indef : Str = pre {"a" ; "an" / strs {"a" ; "e" ; "i" ; "o"}} ;
+
+  LinElem : Type = {s : Str} ;
+  LinProp : Type = {s : Str} ;
+
+  adj1 : Str -> LinElem -> LinProp = 
+    \adj,x -> ss (x.s ++ "is" ++ adj) ;
+  adj2 : Str -> LinElem -> LinElem -> LinProp = 
+    \adj,x,y -> ss (x.s ++ "is" ++ adj ++ y.s) ;
+
+  fun1 : Str -> LinElem -> LinElem = 
+    \f,x -> ss ("the" ++ f ++ "of" ++ x.s) ;
+  fun2 : Str -> LinElem -> LinElem -> LinElem = 
+    \f,x,y -> ss ("the" ++ f ++ "of" ++ x.s ++ "and" ++ y.s) ;
+
+
+} ;