diff options
Diffstat (limited to 'examples/logic/LogicI.gf')
| -rw-r--r-- | examples/logic/LogicI.gf | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf index f8eaf6aa2..1f9b08e41 100644 --- a/examples/logic/LogicI.gf +++ b/examples/logic/LogicI.gf @@ -18,9 +18,9 @@ lincat lin ThmWithProof = theorem ; - Conj A = coord and_Conj A ; - Disj A B = coord or_Conj A B ; - Impl A B = coord ifthen_DConj A B ; + Conj = coord and_Conj ; + Disj = coord or_Conj ; + Impl = coord ifthen_DConj ; Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ; @@ -28,21 +28,21 @@ lin Univ A B = AdvS (mkAdv for_Prep (mkNP all_Predet - (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0))))) + (mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0))))) B ; DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ; DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ; - DisjE A B C c b1 b2 = + DisjE A B C c d e = appendText c (appendText (appendText (cases (mkNum n2)) (proofs - (appendText (assumption A) b1) - (appendText (assumption B) b2))) + (appendText (assumption A) d) + (appendText (assumption B) e))) (proof therefore C)) ; ImplI A B b = |