Using ATP Tools

Part I

Here are three TPTP problems that have already passed the syntax check in the ATP Process. For each one, work your way through the rest of the process until you have reached Happiness, or established it is CSA (countersatisfiable). At each step, save the tool output in a file named ...

PartI_N.sat.txt for a model of the axioms.
PartI_N.thm.txt for a proof of the theorem.
and PartI_N.gdv.txt for a verification trace.
or
PartI_N.csa.txt for a countermodel of the conjecture.

... where N is the problem number below.

Part II

Chuck Schumer needs to prove the following theorem ...

Republicans and Democrats are the only political parties, and they are not the same. All Americans are members of either the Republicans or the Democrats, but not both. The policy of Republicans is capitalism, and the policy of Democrats is socialism. Capitalism and socialism are different policies. An American's policy this that of their party. Mitch McConnell is an American and a Republican. Therefore Mitch McConnell's policy is not socialism.

Convert the scenario to typed first-order logic formulae in TPTP syntax, and save them in the file PartII.p.
Use TPTP4X to check the syntax and format the formulae. Save the formatted version back to PartII.p.txt.
Submit the axioms to a model finder to ensure they are consistent. Save the output in PartII.sat.txt
Submit PartII.p to E. Obtain TPTP format output, and save the (formatted) TPTP format solution in PartII.thm.txt.
Submit PartII.thm.txt for output processing to produce an IDV tree. Save the image in PartII.gif (or whatever image format you use).
Submit PartII.thm.txt for output processing to produce a GDV verification trace. Save the trace in PartII.gdv.txt

Email all the files to me, as attachments.

You must submit your work by email by 16th September. It is worth 15% of the course assessment. I will be graded according to this marking scheme. Please review the policies on assessment in the administration document.