diff --git a/examples/logic/LexTheory.gf b/examples/logic/LexTheory.gf
new file mode 100644
index 000000000..8bdd715a0
--- /dev/null
+++ b/examples/logic/LexTheory.gf
@@ -0,0 +1,8 @@
+interface LexTheory = open Grammar in {
+
+  oper
+    assume_VS : VS ;
+    case_N : N ;
+    have_V2 : V2 ;
+
+}
diff --git a/examples/logic/LexTheoryEng.gf b/examples/logic/LexTheoryEng.gf
new file mode 100644
index 000000000..556bd2b24
--- /dev/null
+++ b/examples/logic/LexTheoryEng.gf
@@ -0,0 +1,7 @@
+instance LexTheoryEng of LexTheory = open GrammarEng,ParadigmsEng,IrregEng in {
+  oper
+    assume_VS = mkVS (regV "assume") ;
+    case_N = regN "case" ;
+    have_V2 = dirV2 have_V ;
+
+}
diff --git a/examples/logic/Theory.gf b/examples/logic/Theory.gf
new file mode 100644
index 000000000..778e0a8ec
--- /dev/null
+++ b/examples/logic/Theory.gf
@@ -0,0 +1,47 @@
+abstract Theory = {
+
+  cat
+    Chapter ;
+    Jment ;
+    [Jment] {0} ;
+    Decl ;
+    [Decl] {0} ;
+    Prop ;
+    Proof ;
+    [Proof] {2} ;
+    Branch ;
+    Typ ;
+    Obj ;
+    Label ;
+    Ref ;
+    [Ref] ;
+    Adverb ;
+    Number ;
+    
+  fun
+    Chap       : Label -> [Jment] -> Chapter ;          -- title, text
+
+    JDefObj    : [Decl] -> Obj -> Obj -> Jment ;        -- a = b (G)
+    JDefObjTyp : [Decl] -> Typ -> Obj -> Obj -> Jment ; -- a = b : A (G)
+    JDefProp   : [Decl] -> Prop -> Prop -> Jment ;      -- A = B : Prop (G)
+    JThm       : [Decl] -> Prop -> Proof -> Jment ;     -- p : P (G)
+
+    DProp      : Prop  -> Decl ;                        -- assume P
+    DPropLabel : Label -> Prop -> Label ;               -- assume P (h)
+    DTyp       : Obj   -> Typ -> Decl ;                 -- let x,y be T
+
+    PProp      : Prop -> Proof ;                        -- P.
+    PAdvProp   : Adverb -> Prop -> Proof ;              -- Hence, P.
+    PDecl      : Decl -> Proof ;                        -- Assume P.
+    PBranch    : Branch -> [Proof] -> Proof ;           -- By cases: P1 P2
+
+    BCases     : Number -> Branch ;                     -- We have n cases.
+    
+    ARef       : Ref -> Adverb ;                        -- by Thm 2
+    AHence     : Adverb ;                               -- therefore
+    AAFort     : Adverb ;                               -- a fortiori
+
+    RLabel     : Label -> Ref ;                         -- Thm 2
+    RMany      : [Ref] -> Ref ;                         -- Thm 2 and Lemma 4
+
+}
diff --git a/examples/logic/TheoryEng.gf b/examples/logic/TheoryEng.gf
new file mode 100644
index 000000000..a45bc0fdd
--- /dev/null
+++ b/examples/logic/TheoryEng.gf
@@ -0,0 +1,10 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+concrete TheoryEng of Theory = TheoryI with
+  (LexTheory = LexTheoryEng), 
+  (Grammar = GrammarEng), 
+  (Symbolic = SymbolicEng), 
+  (Symbol = SymbolEng), 
+  (Combinators = CombinatorsEng), 
+  (Constructors = ConstructorsEng), 
+  ;
\ No newline at end of file
diff --git a/examples/logic/TheoryI.gf b/examples/logic/TheoryI.gf
new file mode 100644
index 000000000..9ab457536
--- /dev/null
+++ b/examples/logic/TheoryI.gf
@@ -0,0 +1,56 @@
+incomplete concrete TheoryI of Theory = 
+  open 
+    LexTheory,
+    Grammar, 
+    Symbolic, 
+    Symbol,
+    Combinators, 
+    Constructors, 
+    (C=ConstructX),
+    Prelude 
+  in {
+
+lincat
+  Chapter = Text ;
+  Jment   = Text ;
+  Decl    = Text ;
+  Prop    = S ;
+  Branch  = S ;
+  Proof   = Text ;
+  [Proof] = Text ;
+  Typ     = CN ;
+  Obj     = NP ;
+  Label   = NP ;
+  Adverb  = PConj ;
+  Ref     = NP ;
+  [Ref]   = [NP] ;
+  Number  = Num ;
+
+lin
+  Chap title jments = 
+    appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
+
+  JDefObj decl a b = 
+    appendText decl (mkUtt (mkS (pred b a))) ;
+
+  DProp p = 
+    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
+  DTyp a ty = --- x pro a: refresh bug
+    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
+
+  PProp p = mkText (mkPhr p) TEmpty ;
+  PAdvProp a p = mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
+  PDecl d = d ;
+  PBranch b ps = mkText (mkPhr b) ps ;
+
+  BCases n = 
+    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet (mkNum n2)) case_N)) ;
+
+  ARef h = mkAdv by8means_Prep h ;
+  AHence = therefore_PConj ;
+  AAFort = C.mkPConj ["a fortiori"] ;
+
+  RLabel h = h ;
+  RMany rs = mkNP and_Conj rs ;
+
+}