Assignment: Tableau-based natural language argument checker for FLASL arguments

COL703: Logic for Computer Science
Assignment: Tableau-based natural language argument checker for FLASL
arguments
Using the datatype for propositional logic arguments as defined in the Assignment 1, implement the tableau
method to
1. verify the validity of propositional logic arguments and
2. give a falsifying truth assignment in case of an invalid argument.
3. Integrate it with the FLASL parser that you implemented in Assignment 1, to obain a FLASL argument
checker. Use the FLASL argument given in the minor exam as a test case and show that you can prove
the validity.
Quick references and test cases.
The datatype definition.
exception Atom_exception
datatype Prop =
ATOM of string |
NOT of Prop |
AND of Prop * Prop |
OR of Prop * Prop |
COND of Prop * Prop |
BIC of Prop * Prop |
ITE of Prop * Prop * Prop
datatype Argument = HENCE of Prop list * Prop
Is this a valid argument? Place the following argument in a text file called god1.flasl
IF ”there is a God” THEN ”God is omniscient” AND ”God is omnipotent”. IF ”God is omniscient”
THEN ”He would know there is Evil”. IF ”God is omnipotent” THEN ”He would prevent Evil”.
”There is Evil”. THEREFORE NOT ”there is a God”.
What about this variation? Place the following argument in a text file called god2.flasl.
”there is a God” IFF ”God is omniscient” AND ”God is omnipotent”. IF ”God is omniscient” THEN
”God would know there is Evil”. IF ”God is omnipotent” THEN ”God would prevent Evil”. ”There
is Evil”. THEREFORE NOT ”there is a God”.
A valid FLASL argument. Place the following argument in a text file called govt1.flasl.
IF ”prices rise” THEN ”the poor and the salaried class will be unhappy”. IF ”taxes are increased”
THEN ”the businessmen will be unhappy”. IF (”the poor and the salaried class are unhappy” OR ”the
businessmen are unhappy”) THEN NOT ”the Government will be re-elected”. ”Inflation rises” IF
”Government expenditure exceeds its revenue”. IF NOT (”taxes are increased” OR ”the Government
resorts to deficit financing” OR ”the Government takes a loan”) THEN ”Government expenditure
will exceed its revenue”. IF ”the Government resorts to deficit financing” THEN ”inflation rises”.
IF ”inflation rises” THEN ”prices rise”. ”the Government will be re-elected”. THEREFORE ”the
Government takes a loan”.
Consider the following conclusion instead. Place the following argument in a text file called govt2.flasl.
Replace the “...” by the body of the previous argument. Is it valid then?
... THEREFORE NOT (”taxes are increased” OR ”the Government resorts to deficit financing”)
Submission details. flasl-tableau.zip This is the only file to be submitted on moodle. It should contain
at least the following files.
tableau implementation. proptableau.sml which contains the actual implementation of the tableau
method.
integration files. Any files that are required for integrating with the FLASL parser of assignment 1
(including a README.txt file if necessary).
Makefile A makefile which integrates the various parts.
FLASL input/output. For any FLASL argument in a text input file inp.flasl your program should
generate an output text file inp.out. Hence for each of the input files god1.flasl, god2.flasl,
govt1.flasl, govt2.flasl, your program should generate the output text files god1.out, god2.out,
govt1.out, govt2.out respectively.