diff options
| author | aarne <aarne@cs.chalmers.se> | 2008-06-25 16:54:35 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2008-06-25 16:54:35 +0000 |
| commit | e9e80fc389365e24d4300d7d5390c7d833a96c50 (patch) | |
| tree | f0b58473adaa670bd8fc52ada419d8cad470ee03 /examples/systemS/README | |
| parent | b96b36f43de3e2f8b58d5f539daa6f6d47f25870 (diff) | |
changed names of resource-1.3; added a note on homepage on release
Diffstat (limited to 'examples/systemS/README')
| -rw-r--r-- | examples/systemS/README | 65 |
1 files changed, 0 insertions, 65 deletions
diff --git a/examples/systemS/README b/examples/systemS/README deleted file mode 100644 index ebbd92ce6..000000000 --- a/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. |