这个作业是用c语言实现命题Tableau

COMP0017. Propositional Tableau implementation in C
Robin Hirsch
November 12, 2019
To be submitted on turnitin by 6th December 2019. Use the skeleton program (posted on
moodle) to create a single file with your C program. Do not use any C libraries other than those
included in the skeleton program.
Your program will read its input from a file called input.txt (an example of input.txt is posted
on moodle), parse each of the ten formulas and output their types, build a tableau for each of the
ten formulas, expand till completed, test to see if they are closed, and then output whether the
formula is satisfiable or not. All the outputs go to a file called output.txt.
If your program correctly parses my input formulas (and says whether they are atomic, negated,
or binary) you’ll get a mark of 40%.. If your program correctly informs me whether the input
formula is satisfiable or not, you’ll get full marks.
1