coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] FOL or SOL formalization in Coq

From: Milad Ketabii <ketabii.math AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] FOL or SOL formalization in Coq
Date: Tue, 18 Dec 2018 07:58:25 +1100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ketabii.math AT gmail.com; spf=Pass smtp.mailfrom=ketabii.math AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk1-f179.google.com
Ironport-phdr: 9a23:otOrhh8PsRJLfP9uRHKM819IXTAuvvDOBiVQ1KB30+wcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDIS9b4sLFeUOIPtToYzjqFsStxSxHgisBOLywTJPhX/5w7E63P46HgHH3QwsBdcOv27IrNX1L6oSXuW1w7PJzTXHdf9ZxTD96I3Rfx0nvPqCU7Vwcc/LxkkuEQPIlk+fqZbqPjOUyOQBqW+b7/BvVe63kG4ntxt+rSSsxsgyhYjGmoIVxUrC9SV23ok5P8G3SEl+YdK8H5tQtj2aN4trQsw5WW1npCE6yrgAtJWmfyYK0IwqywDDZ/GDaYSF4RLuWPyPLTtmmX5pYq+zihS2/EWm1+byTNO70ExQoSpAitTMtm4C1xjU6sWfT/ty5Eah2TKW2wDN6eFIPFk4laTGJ5MjxrM8jJUTsUPEHi/5nEX5krWaeVkj+uit8+jnY7PmqYGAN4JslA3yLqAjlta8DOk4KAQCQXaX9fmm2LH+/0D0RK1GjvgsnanYtJDaK94bpqm8AwJN0YYs9Qq/AC2939QZnHkLNldFdwibj4jpIFzOL/X4Au2+g1Soijtk2/fGPrj5DpXXMnfDiKvhfap660NE1AUzyslf64tIBbEFPfL8QVT8tMfYDx88Kwy72fzrCNR71oMEWGKAGLWVMK3IsQzA2uV6KO6VIYQRpTzVKv4/5veog2Vqt0UaePyM3J8eZDibE+hvKUSYKS7vj8sIG2YL+A83UOzCh1iLUDoVbHG3CfFvrgonAZ6rWN+QDrumh6aMiX/iT89mI1teA1XJKk/GMoCNWvMCciWXe5YznTkNVLznQIgkh0j36F3KjoF/J++RwRU28Ir53YEsteLWnBA2szdzCpbFijzffyRPhmoNAgQO8uV/rEh6kAnR1KF5h7lGFoUW6aoWA0E1MpnTy+E8ANf3CFrM

Hi Francisco

There is also some SOL formalised in Coq by Caitlin D'Abrera, which you can find here.

bests

Milad

On Tue, Dec 18, 2018 at 3:10 AM roux cody <cody.roux AT gmail.com> wrote:

Hi Francisco,

There have been many such formalizations, as a few google searches will show. One of note would be O'Connor's proof of incompleteness: https://arxiv.org/pdf/cs/0505034.pdf

You might also take a look at this stackexchange answer: https://cstheory.stackexchange.com/a/10087/3984

Best,
Cody

On Mon, Dec 17, 2018 at 10:41 AM Francisco Trucco <franciscoctrucco AT gmail.com> wrote:
Hi all,

I was wondering if any of you knew of a first order logic or second order logic formalization in Coq. In particular, I am looking for something similar to Coq in Coq but with FOL or SOL.

Thanks a lot!

Francisco Trucco

[Coq-Club] FOL or SOL formalization in Coq, Francisco Trucco, 12/17/2018
- Re: [Coq-Club] FOL or SOL formalization in Coq, roux cody, 12/17/2018
  - Re: [Coq-Club] FOL or SOL formalization in Coq, Milad Ketabii, 12/17/2018
- Re: [Coq-Club] FOL or SOL formalization in Coq, Yannick Forster, 12/17/2018