GDV-LP = GDV + LambdaPi
GDV
- Relies on trusted ATP
- You don't trust ATP, but you trust Dedukti?
Ekstrakto
- Uses ZenonModulo as the trusted prover
- ZenonModulo generates LambdaPi terms
- LambdaPi terms checked in the Dedukti framework
- Only CNF derivations
GDV-LP
- Does all the GDV goodness
- Uses ZenonModulo as the trusted prover
- ZenonModulo generates LambdaPi terms
- LambdaPi terms checked in the Dedukti framework
- For CNF and FOF (so far)
Work in Progress
- Verification of Skolemization steps using SKonverto
- Typed First-Order (TF0) derivations