Thursday 2 March 2017, 9:00: Tactics and certificates in Meta Dedukti, Raphaël Cauderlier (IRIF).
Tactics are often featured in proof assistants to simplify the
interactive development of proofs by allowing domain-specific
automation. Moreover, tactics are also helpful to check the output of
automatic provers which often omit details.
We use meta-programming to define a tactic language for Dedukti which can be used both for checking certificates produced by automatic provers and for developing Dedukti proofs interactively.
More precisely, we propose a dependently-typed tactic language for first-order logic in Meta Dedukti and an untyped certificate language built on top of the tactic language.