Develop maintainable tooling in Isabelle/GD to export verified GD proofs into a minimalistic "kernel" syntax, perhaps based on predicate grounded arithmetic (PGA) for example. The heavy-duty automated reasoning tools should always be able to produce correct proofs in this syntax whenever they claim to find a proof at all; otherwise there's a bug.
Then we have two high-priority "consumers" for this kernel syntax:
- A minimal checker for GA kernel proofs - ideally itself designed for verification, e.g., implemented in HOL or Coq with support for export to executable checker code in conventional languages.
- A yacc-like translator that takes GA kernel proofs and produces corresponding Isabelle/HOL code intended to be dropped into the GA metatheory framework as HOL proofs of the form "GA proves theorem T".
Once consumer #1 above is implemented, set up regression testing tooling to verify that the GA-kernel-export of all our maintained GD theory files works correctly and produces GA kernel proofs that the minimal checker successfully verifies (in at least vaguely acceptable time).
Develop maintainable tooling in Isabelle/GD to export verified GD proofs into a minimalistic "kernel" syntax, perhaps based on predicate grounded arithmetic (PGA) for example. The heavy-duty automated reasoning tools should always be able to produce correct proofs in this syntax whenever they claim to find a proof at all; otherwise there's a bug.
Then we have two high-priority "consumers" for this kernel syntax:
Once consumer #1 above is implemented, set up regression testing tooling to verify that the GA-kernel-export of all our maintained GD theory files works correctly and produces GA kernel proofs that the minimal checker successfully verifies (in at least vaguely acceptable time).