coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to prove false

From: Stefan Ciobaca <stefan.ciobaca AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] how to prove false
Date: Wed, 25 Mar 2015 09:05:51 +0200

The development is here:

https://github.com/clarus/falso

From the readme:

"This is an implementation in the Coq proof assistant of the Falso proof system. It exploits a bug of thevm_compute command when there is a type with more than 255 constructors. The vm_computecommand evaluates a term efficiently by compilation to a byte-code. This bug concerns all recent versions of Coq, including Coq 8.4pl5."

Cheers,
Stefan Ciobaca

[Coq-Club] how to prove false, Stefan Ciobaca, 03/25/2015
- Re: [Coq-Club] how to prove false, Jonathan Leivent, 03/25/2015
  - Re: [Coq-Club] how to prove false, Jacques-Henri Jourdan, 03/25/2015
    - Re: [Coq-Club] how to prove false, Jonathan Leivent, 03/25/2015
      - Re: [Coq-Club] how to prove false, Laurent Théry, 03/25/2015
        
        Re: [Coq-Club] how to prove false, Jonathan Leivent, 03/25/2015
        
        Re: [Coq-Club] how to prove false, Laurent Théry, 03/25/2015
        
        Re: [Coq-Club] how to prove false, Matthieu Sozeau, 03/25/2015