Added README and LICENSE.

LICENSE

@@ -0,0 +1,14 @@
+Copyright (C) Sarah Mount, 2010.
+
+This program is free software; you can redistribute it and/or
+modify it under the terms of the GNU General Public License
+as published by the Free Software Foundation; either version 2
+of the License, or (at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have rceeived a copy of the GNU General Public License
+along with this program.  If not, see <http://www.gnu.org/licenses/>.

README

@@ -0,0 +1,63 @@
+
+This is a simple tautology checker, written in Java, as a teaching
+tool.
+
+It uses an operator-precendence parser to parse a file containing a
+proposition and print out a trace which contains the syntax tree of
+the original proposition, its negative normal form, conjunctive normal
+form and whether or not the proposition is a tautology.
+
+The language parse by the checker is the following:
+
+Prop ::= FF
+       | TT
+       | NOT Prop
+       | Prop AND Prop
+       | Prop OR Prop
+       | Prop => Prop
+       | Prop AND Prop
+       | ( Prop )
+
+There are a number of examples in the tests/ directory and a UNIX
+shell script (check.sh) which takes a file name and calls the checker.
+
+For example:
+
+$ javac checker/Checker.java 
+$ java checker.Checker tests/peirces_law.prop 
+
+	 A Tautology Checker for Propositional Calculus
+	------------------------------------------------
+
+Input file: tests/peirces_law.prop
+----------
+((P => Q)=>P)=>P
+
+
+
+Abstract syntax tree:
+--------------------
+((P => Q) => P) => P
+
+RESULT OF formula.removeImplications():
+--------------------------------------
+(!(!(!P \/ Q) \/ P) \/ P)
+
+RESULT OF formula.toNnf():
+-------------------------
+(((!P \/ Q) /\ !P) \/ P)
+
+RESULT OF formula.nnfToCnf():
+----------------------------
+(((!P \/ Q) \/ P) /\ (!P \/ P))
+
+RESULT OF formula.simplifyCnf():
+-------------------------------
+TRUE
+
+Your formula is a tautology.
+
+$ 
+
+
+-- Sarah Mount 2010.