From 25b31684378d3b0668b65939fc7b30b0c1e8d130 Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Tue, 20 Dec 2005 14:20:42 +0000
Subject: CS's system S

---
 examples/systemS/README | 65 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 examples/systemS/README

(limited to 'examples/systemS/README')

diff --git a/examples/systemS/README b/examples/systemS/README
new file mode 100644
index 000000000..ebbd92ce6
--- /dev/null
+++ b/examples/systemS/README
@@ -0,0 +1,65 @@
+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