coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Decidability of Propositional Logic
Date: Sat, 28 Nov 2015 10:26:34 +0000
Accept-language: en-GB, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jeffrey.terrell AT kcl.ac.uk; spf=Pass smtp.mailfrom=jeffrey.terrell AT kcl.ac.uk; spf=Pass smtp.helo=postmaster AT emea01-db3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:rXEjnRYLSrhircQcvvss8xD/LSx+4OfEezUN459isYplN5qZpcS4bnLW6fgltlLVR4KTs6sC0LqL9fC8EjVcvN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvc2PKFwU2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1AbSy09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGHo06pxUhLsjGNPFTM3/nvam4Y42KBWrhy7qg0534POeoyRMNJ9daebdNhcWGkXDZUZbDBIHo7pN9hHNOEGJ+sN6tCl/1Y=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:23

Does anyone know of a Coq proof that propositional logic is decidable?

[Coq-Club] Decidability of Propositional Logic, Terrell, Jeffrey, 11/28/2015
- Re: [Coq-Club] Decidability of Propositional Logic, Julian Michael, 11/28/2015
- Re: [Coq-Club] Decidability of Propositional Logic, Emilio Jesús Gallego Arias, 11/29/2015
  - Re: [Coq-Club] Decidability of Propositional Logic, Daniel Schepler, 11/29/2015
    - Re: [Coq-Club] Decidability of Propositional Logic, Julian Michael, 11/29/2015
      - Re: [Coq-Club] Decidability of Propositional Logic, Gabriel Scherer, 11/29/2015
        
        Re: [Coq-Club] Decidability of Propositional Logic, Julian Michael, 11/29/2015
- Re: [Coq-Club] Decidability of Propositional Logic, Gert Smolka, 11/29/2015