coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Decidability of Propositional Logic

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Decidability of Propositional Logic
Date: Sun, 29 Nov 2015 14:52:32 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=smolka AT ps.uni-saarland.de; spf=None smtp.mailfrom=smolka AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT theia.rz.uni-saarland.de
Ironport-phdr: 9a23:sHNRNBcv9UTlKnirb4HgoxqRlGMj4u6mDksu8pMizoh2WeGdxc6+ZB7h7PlgxGXEQZ/co6odzbGG7uawByddv96oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvc2NKFgWzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB0obiAYAOA3C6BLzFsPqtyz+teNVwDLcIMv3CKs9UC6m5qFnDhPl3nRUfwUl+X3a35QjxJlQpwis8kRy

> On 28 Nov 2015, at 11:26, Terrell, Jeffrey
> <jeffrey.terrell AT kcl.ac.uk>
> wrote:
>
> Does anyone know of a Coq proof that propositional logic is decidable?
>

You find decidability proofs both for classical and intuitionistic
propositional logic in the lecture notes for “Introduction to Computational
Logic”, see https://www.ps.uni-saarland.de/courses/cl-ss14/script/icl.pdf,
Chapters 11 and 12. There only the fragment with implication and falsity is
treated. You find Coq proofs for the case with all connectives at
https://www.ps.uni-saarland.de/~dang/ri-lab.php.

[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