From 5c713d8f027a9b6be687ee3f7e917e8bd2115773 Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Fri, 27 Jun 2008 09:18:50 +0000
Subject: took away old-examples

---
 old-examples/systemS/README | 65 ---------------------------------------------
 1 file changed, 65 deletions(-)
 delete mode 100644 old-examples/systemS/README

(limited to 'old-examples/systemS/README')

diff --git a/old-examples/systemS/README b/old-examples/systemS/README
deleted file mode 100644
index ebbd92ce6..000000000
--- a/old-examples/systemS/README
+++ /dev/null
@@ -1,65 +0,0 @@
-AR 20/12/2005
-
-This is a translator of a part of the proof system
-by Claes Strannegård, as defined in the manuscript
-"Translating Formal Proofs into English".
-
-The functionality is to translate between a formal
-and an informal notation for proofs.
-
-As examples, we provide 3 of the 4 examples in
-Strannegård's paper. His example 3 is left as exercise.
-
-A good way to start is
-
-  % gf <test.gfs
-
-which will translate the proofs back and forth.
-
-If you modify the grammars and want to compile from source, you also need
-
-  % export GF_LIB_PATH=/home/aarne/GF/lib -- set to the path in your system
-
-Files:
-
-  ex1eng.txt      -- the 3 tests
-  ex1.txt    
-  ex2eng.txt
-  ex2.txt
-  ex4eng.txt
-  ex4.txt
-
-  Formula.gf      -- abstract syntax of formulas
-  FormulaSymb.gf  -- concrete syntax of formulas
-  Precedence.gf   -- precedence package
-  ProofEng.gf     -- top concrete syntax, English
-  Proof.gf        -- top abstract syntax
-  ProofSymb.gf    -- top concrete syntax, symboli
-
-  proof.gfcm      -- precompiled translator
-
-  README          -- this file
-  test.gfs        -- the test script
-
-
-Notes:
-
-1. The abstract syntax does not do proof checking.
-
-2. de Morgan labels have been disambiguated with "1" and "2".
-
-3. The symbolic Ex falso quodlibet rule needs to show the
-   conclusion formula in the label to make linearization 
-   possible (in the absence of smart proof checking).
-
-4. The English concrete syntax needs some extra formula
-   arguments for the same reason. These arguments can be
-   omitted, but the resulting parser returns some 
-   metavariables.
-
-An interesting further task would be to implement the
-proof checker and a proof search procedure, in Haskell or,
-even better, in the GF Transfer Language.
-
-Another nice thing would be to linearize the formulas
-into real English.
-- 
cgit v1.2.3