Using ATP Tools

Mitt Romney and Barrack Obama need to prove the following theorem ...

Republicans and Democrats are political parties. All Americans are members of only the Republicans or the Democrats. 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. Bill is an American. Bill is a Republican. Therefore Bill's policy is not socialism.

1. Convert the scenario to logic formulae (use the "mathematical" notation, e.g., ∀ for "for all"), and use any word processing system to create a PDF of the formulae, named Problem.pdf.

2. Convert the formula to TPTP syntax, and save them in the file Problem.p. Use TPTP4X to check the syntax and format the formulae. Save the formatted version back to Problem.p.

3. Submit the axioms to Paradox, to ensure they are consistent. Save the Paradox output in Problem.sat

4. Submit Problem.p to EP. Obtain TPTP format output, and save the TPTP format solution in EP.s.

5. Submit EP.s for output processing to produce a IDV tree. Save the image in EP.gif (or whatever image format you use).

6. Submit EP.s for output processing to produce a GDV verification trace. Save the trace in EP.gdv

7. Use TPTP2X or TPTP4X to add all the axioms of equality to Problem.p and save in Equality.p.

8. Use ECNF to convert Problem.p to CNF and save in CNF.p.

Email all the files to me, as attachments.

You must submit your work by email by 20th February. It is worth 10% of the subject's assessment. Please review the policies on assessment in the administration document.