diff options
| author | Hugo Herbelin | 2015-12-01 16:30:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 10:10:43 +0100 |
| commit | 6b39f9904b4e9d5260c4fd97ff10e52c489c6051 (patch) | |
| tree | 1758401db83703593b3de7c3548a7be4aff3eacc /dev | |
| parent | aa99912e9adc566a179b4972ff85a92b967fb134 (diff) | |
Adding proofs on the relation between excluded-middle and minimization.
In particular, a proof of the equivalence of excluded-middle and an
unrestricted principle of minimization.
Credits to Arnaud Spiwack for the ideas and formalizations of the proofs.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions