GDV + LambdaPi = GDV-LP

• Relies on trusted ATP
• You don't trust ATP, but you trust Dedukti?

• Does all the GDV goodness
• Uses ZenonModulo as the trusted prover
  • ZenonModulo generates LambdaPi terms
• LambdaPi terms checked in the Dedukti framework
  • Each LambdaPi file requires it's parent files
• For CNF, FOF, and TFF (so far)

Work in Progress

• Merging the LambdaPi terms
• Large scale testing
• Verification of Skolemization steps
• THF using Leo-III instead of ZenonModulo