ATP System Implementation

• Indirect proofs for FDE/A3/RM3
  • Problems translated to FOL
  • Solved with FOL automated reasoning tools
  • No translation of proofs/models

• A shell Script
  • Translation implemented in Prolog
  • Proof by a FOL theorem prover
  • Countermodel by a FOL finite model finder

• Parameters
  • Which logic - FDE or A3 or RM3
  • Which conditional connective for FDE
  • CPU time limit
  • List of FOL theorem provers (currently Vampire 4.2)
  • List of FOL model finders (currently Vampire 4.2 in FMo mode)
  • Percentage of time for each FOL system (currently 80% and 20%)