coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is Coq appropriate as logical framework for non-monotonic, defeasible, adaptable, categorical logics?

From: Alex Meyer <alex153 AT outlook.lv>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Is Coq appropriate as logical framework for non-monotonic, defeasible, adaptable, categorical logics?
Date: Sat, 22 Apr 2017 23:31:35 +0000
Accept-language: lv-LV, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=alex153 AT outlook.lv; spf=Pass smtp.mailfrom=alex153 AT outlook.lv; spf=Pass smtp.helo=postmaster AT EUR03-AM5-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:qhjMwh2tKAANqgaGsmDT+DRfVm0co7zxezQtwd8Zse0VKfad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJ/kK1UrQm7qBBj34LZep2ZOOZgcq7bYNgURXBBXsFUVyFZHo68a5UADuUcNuhfsYb8p0UBrQGjDgSrHuzvziFHh3Dr0aA63eksCgbG3BE8H9IKt3TUq9b1OL0WUeCr1aTFyyjIYfBO2Trl54XEbgotrPWSUb5qc8fd1VMjGgzHg1iWtIfrJSma1v4XvGie9+dgVfygi2ogqwxprTagyNsihpXHi44M1l3K8iV0zJ8yJdKjVkF3e9mkEIZMty6BMIt2X8UiTHxytCYi0L0GvoK7czYWx5Q7xh7fbPqHf5KP4hL+SOaRJTB4hHVmeL6lmxmy9k2gxvX9VsmyzllKsjJIn9bQunwX0xHf9NKLR/lh8ku71juC1Rjf6uReLkA1karbJYQhwrk1lpcLq0vDGjH5mUrrgKKWeEgp4e+o6/n7YrXioZ+cMIx0hhv6MqQwgsC/G/g3MhASX2iH/uSxzKHs/UrgQLlTkvI2lrTZv4vBKMQApq+5BhdV3Zw55xa+CTemytUYkmMdIFJLYhLUx7TubhvFJ+m9BvOiiXytli1qzrbIJPepVp7KNz3IlKrrVbd78U9VjgQpm4Nx/ZVRX5gFLeK7f0LgucaQWhY9Phztnr3PD8hh0oQZWiSLHPnKY+vprVaU67d3cKG3b4gPtWOlJg==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi!

I am learning about logics that are used for legal reasoning and commonsense reasoning - like non-monotonic, defeasible, adaptable (and also categorical) logics. Can Coq be used as logical framwork for implementing those logics?

And generally - are there logics that can not be implemented in Coq and what should be added to Coq to make it into logical framework for those logics as well?

And even more generally - logics are only one kind of reasoning - deductive reasoning. What about other types of reasoning - abductive, inductive and analogical - and Coq?

Sorry for newbie question but there I can hope to receive the most conscise answers on these topics. Thanks.

[Coq-Club] Is Coq appropriate as logical framework for non-monotonic, defeasible, adaptable, categorical logics?, Alex Meyer, 04/23/2017
- Re: [Coq-Club] Is Coq appropriate as logical framework for non-monotonic, defeasible, adaptable, categorical logics?, Emilio Jesús Gallego Arias, 04/23/2017