diff --git a/grammars/logic/ArithmFre.gf b/grammars/logic/ArithmFre.gf
new file mode 100644
index 000000000..fcc99f4e9
--- /dev/null
+++ b/grammars/logic/ArithmFre.gf
@@ -0,0 +1,37 @@
+--# -path=.:../prelude
+
+concrete ArithmFre of Arithm = LogicFre ** open ResFre in {
+
+lin Nat = {g = masc ; s = nomReg "nombre"} ;
+zero = {g = masc ; s = table {c => (prep ! c) ++ "zéro"}} ;
+succ n =
+  {g = masc ; s = table {c => defin ! sg ! masc ! c ++ "successeur" ++ n.s ! dd}} ;
+EqNat k n = mkPropA2 aa k (adjAl "éga") n ;
+LtNat k n = mkPropA2 aa k (adjReg "inférieur") n ;
+Div k n = mkPropA2 nom k (table {_ => nomReg "divisible"}) n ; --- par !
+
+Even n = mkPropA1 n (adjReg "pair") ;
+Odd n = mkPropA1 n (adjReg "impair") ;
+Prime n = mkPropA1 n (adjEr "premi") ;
+
+lin one  =
+  {g = masc ; s = table {c => (prep ! c) ++ "un"}} ;
+lin two  =
+  {g = masc ; s = table {c => (prep ! c) ++ "deux"}} ;
+lin sum m n = {g = fem ; s = table {
+  c => defin ! sg ! fem ! c ++ "somme" ++ m.s ! dd ++ "et" ++ n.s ! dd}} ;
+lin prod m n = {g = masc ; s = table {
+  c => defin!sg!fem!c ++ "produit" ++ m.s ! dd ++ "et" ++ n.s ! dd}} ;
+lin evax1  =
+  {s = "par"++"le"++"premier"++"axiome"++"de"++"parité,"++"zéro"++"est"++"pair"} ;
+lin evax2 n c =
+  {s = c.s ++ "."++"Par"++"le"++"deuxième"++"axiome"++"de"++"parité,"++"le"++"successeur" ++ (n.s ! dd) ++ "est"++"impair"} ;
+lin evax3 n c =
+  {s = c.s ++ "."++"Par"++"le"++"troisième"++"axiome"++"de"++"parité,"++"le"++"successeur" ++ (n.s ! dd) ++ "est"++"pair"} ;
+lin eqax1  =
+  {s = "par"++"le"++"premier"++"axiome"++"d'égalité,"++"zéro"++"est"++"égal"++"a"++"lui-même"} ;
+lin eqax2 m n c =
+  {s = c.s ++ "."++"Par"++"le"++"deuxième"++"axiome"++"d'égalité,"++"le"++"successeur" ++ (m.s ! dd) ++ "est"++"égal"++"au"++"successeur" ++ n.s ! dd} ;
+lin IndNat C d e =
+  {s = "nous"++"nous"++"servons"++"d'induction."++"Pour"++"la"++"base," ++ d.s ++ "."++"Pour"++"le"++"pas"++"d'induction,"++"considérons"++"un"++"nombre" ++ e.$0 ++ "et"++"supposons" ++ que ++ (C.s ! ind) ++ "(" ++ e.$1 ++ ")" ++ "." ++ e.s ++ "Donc,"++"pour"++"tous"++"les"++"nombres" ++ C.$0 ++ "," ++ C.s ! ind} ;
+}
diff --git a/grammars/logic/LogicFre.gf b/grammars/logic/LogicFre.gf
new file mode 100644
index 000000000..65beb56ae
--- /dev/null
+++ b/grammars/logic/LogicFre.gf
@@ -0,0 +1,84 @@
+concrete LogicFre of Logic = open ResFre, Prelude in {
+
+flags lexer=vars ; unlexer=text ;
+
+lincat 
+Text = {s : Str} ;
+Dom = {g : Gen ; s : Num => Str} ;
+Prop = LinProp ;
+Elem = LinElem ;
+Proof = {s : Str} ;
+
+lindef Elem = \e -> {g = masc ; s = table {c => prep ! c ++ e}} ;
+
+lin
+Statement A = 
+  {s = A.s ! ind ++ "."} ;
+ThmWithProof A a =
+  {s = "Théorème"++"." ++ (A.s ! ind) ++ "."++ PARA ++ "Démonstration"++"." ++ a.s ++ "."} ;
+ThmWithTrivialProof A a =
+  {s = "Théorème"++"." ++ (A.s ! ind) ++ "."++ PARA ++ "Démonstration"++"."++"Triviale"++"."} ;
+Disj A B =
+  {s = table {m => (A.s ! m) ++ "ou" ++ B.s ! m}} ;
+Conj A B =
+  {s = table {m => (A.s ! m) ++ "et" ++ B.s ! m}} ;
+Impl A B =
+  {s = table {m => si ++ (A.s ! ind) ++ "alors" ++ B.s ! m}} ;
+Univ A B =
+  {s = table {m => "pour" ++ tout ! A.g ! pl ++ "les" ++ A.s ! pl ++ B.$0 ++ "," ++ B.s ! m}} ;
+Exist A B =
+  {s = table {m => "il"++"existe" ++ indef ! A.g ++ A.s ! sg ++ B.$0 ++ 
+        tel ! A.g ! sg ++ que ++ B.s ! subj}} ;
+Abs  =
+  {s = table {{ind} => "nous"++"avons"++"une"++"contradiction" ; {subj} => "nous"++"ayons"++"une"++"contradiction"}} ;
+Neg A =
+  {s = table {m => "il" ++ ne ++ etre ! sg ! m ++ "pas"++"vrai" ++ que ++ A.s ! subj}} ;
+ImplP A B =
+  {s = table {m => si ++ (A.s ! ind) ++ "alors" ++ B.s ! m}} ;
+ConjI A B a b =
+  {s = a.s ++ "." ++ b.s ++ "."++"Donc" ++ (A.s ! ind) ++ "et" ++ B.s ! ind} ;
+ConjEl A B c =
+  {s = c.s ++ "."++"A"++"fortiori," ++ A.s ! ind} ;
+ConjEr A B c =
+  {s = c.s ++ "."++"A"++"fortiori," ++ B.s ! ind} ;
+DisjIl A B a =
+  {s = a.s ++ "."++"A"++"fortiori," ++ (A.s ! ind) ++ "ou" ++ B.s ! ind} ;
+DisjIr A B b =
+  {s = b.s ++ "."++"A"++"fortiori," ++ (A.s ! ind) ++ "ou" ++ B.s ! ind} ;
+DisjE A B C c d e =
+  {s = c.s ++ "."++
+       "Nous"++"avons"++"deux"++"possibilités."++ 
+       "Premièrement,"++ "supposons" ++ que ++ A.s ! ind ++ "(" ++ d.$0 ++ ")" ++ 
+       "." ++ d.s ++ "."++
+       "Deuxièmement,"++ "supposons" ++ que ++ B.s ! ind ++ "(" ++ e.$0 ++ ")" ++ 
+       "." ++ e.s ++ "."++"Donc" ++ (C.s ! ind) ++ "dans"++"les"++"deux"++"cas"} ;
+ImplI A B b =
+  {s = "supposons" ++ que ++ A.s ! ind ++ "(" ++ b.$0 ++ ")" ++ "." ++ b.s ++ "."++
+       "Donc"++"," ++ si  ++ A.s ! ind ++ "alors" ++ B.s ! ind} ;
+ImplE A B c a =
+  {s = a.s ++ "."++"Mais" ++ c.s ++ "."++"Donc" ++ B.s ! ind} ;
+NegI A b =
+  {s = "supposons" ++ que ++ A.s ! ind ++ "(" ++ b.$0 ++ ")" ++ "." ++ b.s ++ "." ++
+       ["Donc , il n'est pas vrai"] ++ que ++ A.s ! subj} ;
+NegE A c a =
+  {s = a.s ++ "."++"Mais" ++ c.s ++ "." ++ ["Nous avons une contradiction"]} ;
+UnivI A B b =
+  {s = "considérons" ++ indef ! A.g ++ A.s ! sg ++ b.$0 ++ "arbitraire." ++ 
+       b.s ++ "."++"Donc"++","++"pour" ++ tout ! A.g ! pl ++ 
+       "les" ++ A.s ! pl ++ B.$0 ++ "," ++ B.s ! ind} ;
+UnivE A B c a =
+  {s = c.s ++ "."++
+       "Donc" ++ B.s ! ind ++ "avec" ++ B.$0 ++ "remplacé" ++ "par" ++ a.s ! nom} ;
+ExistI A B a b =
+  {s = b.s ++ "."++"Donc"++"il"++"existe" ++ indef ! A.g ++ A.s ! sg ++ B.$0 ++ 
+       tel ! A.g ! sg ++ que ++ B.s ! subj} ;
+ExistE A B C c d =
+  {s = c.s ++ "."++"Considérons" ++ indef ! A.g ++ A.s ! sg ++ d.$0 ++ 
+       ["arbitraire , et supposons"] ++ que ++ B.s ! ind ++ "(" ++ d.$1 ++ ")" ++ 
+       "." ++ d.s ++ "."++"Donc" ++ C.s ! ind ++ "indépendamment" ++ "de" ++ d.$0} ;
+AbsE C c =
+  {s = c.s ++ "." ++ "Nous" ++ "concluons" ++ que ++ C.s ! ind} ;
+Hypo A a =
+  {s = "par"++"l'hypothèse" ++ a.s ++ "," ++ A.s ! ind} ;
+Pron A _ = {s = pronom ! A.g ; g = A.g} ;
+} ;
\ No newline at end of file
diff --git a/grammars/logic/ResFre.gf b/grammars/logic/ResFre.gf
new file mode 100644
index 000000000..7283e9fcd
--- /dev/null
+++ b/grammars/logic/ResFre.gf
@@ -0,0 +1,78 @@
+resource ResFre = {
+param 
+Gen = masc  | fem  ;
+Num = sg  | pl  ;
+Mod = ind  | subj  ;
+Cas = nom  | aa  | dd  ;
+
+oper 
+nomReg : Str -> Num => Str = \str -> table {{sg} => str ; {pl} => str + "s"} ;
+adjReg : Str -> Gen => Num => Str = \str -> 
+  table {{masc} => nomReg str ; {fem} => nomReg (str + "e")} ;
+adjEl : Str -> Gen => Num => Str = \str ->
+  table {{masc} => nomReg str ; {fem} => nomReg (str + "le")} ;
+adjAl : Str -> Gen => Num => Str =  \str ->
+  table {{masc} => table {{sg} => str + "l" ; {pl} => str + "ux"} ; 
+       {fem}  => nomReg (str + le) } ;
+adjEr : Str -> Gen => Num => Str = \str ->
+  table {{masc} => nomReg (str + "er") ; {fem}  => nomReg (str + "ère")} ;
+
+LinElem = {g : Gen ; s : Cas => Str} ;
+LinProp = {s : Mod => Str} ;
+
+voyelle : Strs = strs {"a" ; "e" ; "i" ; "o" ; "u" ; "y" ; "é"} ;
+elision : Str = pre {"e" ; "'" / voyelle} ;
+ne : Str = "n" + elision ;
+de : Str = "d" + elision ;
+le : Str = "l" + elision ;
+que : Str = "qu" + elision ;
+
+si : Str = pre {"si" ; "s'" / strs {"il" ; "ils"}} ;
+indef : Gen => Str = table {{masc} => "un" ; _ => "une"} ;
+tel : Gen => Num => Str = adjEl "tel" ;
+tout : Gen => Num => Str =
+  table {{masc} => table {{sg} => "tout" ; {pl} => "tous"} ; {fem} => nomReg "toute" } ;
+etre : Num => Mod => Str = formVerbe "est" "soit" "sont" "soient" ;
+
+formVerbe : Str -> Str -> Str -> Str -> Num => Mod => Str = 
+ \sgi -> \sgs -> \pli -> \pls ->
+  table {{sg} => table {{ind} => sgi ; {subj} => sgs} ; 
+       {pl} => table {{ind} => pli ; {subj} => pls}} ; 
+prep : Cas => Str =
+  table {{nom} => [] ; {aa} => "à" ; {dd} => de} ;
+
+defin : Num => Gen => Cas => Str =
+  table {
+   {sg} => table {
+     {masc} => table {
+         {dd}  => pre {"du" ; "de"++"l'" / voyelle} ; 
+         {aa}  => pre {"au" ; "à"++"l'" / voyelle} ;
+         c     => prep ! c ++ le
+                   } ;
+     {fem}  => table {
+         c     => prep ! c ++ pre {"la" ; "l'" / voyelle} 
+                   }
+               } ;
+   {pl} => table {
+     _     => table {
+         {dd}  => "des" ; 
+         {aa}  => "aux" ;
+         c     => prep ! c ++ "les"
+                  }
+               }
+  } ;
+
+pronom : Gen => Cas => Str = table {
+  masc => table {nom => "il" ; c => prep ! c ++ "lui"} ;
+  fem  => table {c => prep ! c ++ "elle"} 
+  } ;
+
+mkPropA1 : LinElem -> (Gen => Num => Str) -> LinProp = \elem -> \adj ->
+ {s = table {m => elem.s ! nom ++ etre ! sg ! m ++ adj ! elem.g ! sg}} ;
+
+mkPropA2 : Cas -> LinElem -> (Gen => Num => Str) -> LinElem -> LinProp = 
+ \cas -> \elem -> \adj -> \elem2 -> let 
+   {adjP : Gen => Num => Str = table {g => table {n => adj ! g ! n ++ elem2.s ! cas}}}
+ in mkPropA1 elem adjP ;
+
+}