Friday 22 April 2016, 10:30: Automated constructivisation of proofs, Frédéric Gilbert (Inria/CEA/NASA).

Determining whether a classical theorem can be proved constructively is well-known to be undecidable. However, it is possible in practice to turn a large amount of classical proofs into constructive ones. In this presentation, we show a new constructivisation algorithm for first order logic, along with its implementation in the automated theorem prover Zenon.