What is Proved
From What to What
- Provide the "from" system as 1st order axioms
- Provide each axiom and rule of the "to" system as conjectures
- HELP! Do the rules have to be proved?
TPTP Files
- Take advantage of TPTP's multiple conjecture semantics
- Example:
S5=S1-0M6S3M9B_to_S5=KM5.p
- Submit via SystemOnTPTP
- Generally, definitional approach makes life harder for ATP
- Proving a defined name from the same axiom is trivial