JGXYZ Implementation

• Indirect proofs for XYZ
  • Unary and binary truth tables provided, e.g., FDE^→_cmi
  • 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
  • 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%)

• Available online in SystemOnTPTP