Email Gateway (Aug 22 2022 at 20:26): Email Gateway (Aug 22 2022 at 20:26):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear all,
are there the diamond and box operators from modal logic ("possibly",
"necessarily" resp.) anywhere defined in the AFP or in the Library?
Many thanks,
Best,
Angeliki
Email Gateway (Aug 22 2022 at 20:26):From: Tobias Nipkow <nipkow@in.tum.de>
On 21/08/2019 02:48, Dr A. Koutsoukou-Argyraki wrote:
Dear all,
are there the diamond and box operators from modal logic ("possibly",
"necessarily" resp.) anywhere defined in the AFP or in the Library?
There is an entry Linear Temporal Logic https://www.isa-afp.org/entries/LTL.html
Tobias
Many thanks,
Best,
Angeliki
Email Gateway (Aug 22 2022 at 20:26):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Christoph Benzmüller has some papers on formalizing modal logic:
http://page.mi.fu-berlin.de/cbenzmueller/papers/bibtexbrowser.local.php?fram
eset&bib=chris.bib&type=.*
I don't know whether the files are available in the AFP or the library.
Email Gateway (Aug 22 2022 at 20:27):From: Joao Marcos <botocudo@gmail.com>
Hi, Angeliki:
are there the diamond and box operators from modal logic ("possibly",
"necessarily" resp.) anywhere defined in the AFP or in the Library?
Some 15 years ago I had a paper on automating and experimenting with
labelled natural deduction for a couple of normal modal logics (and
also some hybrid logics):
https://tinyurl.com/yym7ymnp
The corresponding theories have not been ported from Isabelle 2005,
though, and results have not been submitted to the AFP. Maybe they
will be considered useful again, nonetheless, as hardcore
proof-theorists seem finally to have embraced labelled deduction.
Yours, Joao Marcos
Email Gateway (Aug 22 2022 at 20:28):From: Tjark Weber <tjark.weber@it.uu.se>
Angeliki,
In addition to what was mentioned already, there is also an AFP entry
on Modal Logics for Nominal Transition Systems:
https://www.isa-afp.org/entries/Modal_Logics_for_NTS.html
This deals with transitions that can bind names, and features
infinitary formulas, so (depending on what your goal is) it may be a
bit over the top. I am just mentioning it for completeness.
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Aug 22 2022 at 20:28):From: Tobias Nipkow <nipkow@in.tum.de>
Let me also advertise the Search button on the AFP home page: if you type in
"modal", it finds Tjark's entry as the second item on its list.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 20:28):From: Andreas Halkjær From <andro.from@gmail.com>
My Epistemic Logic entry defines the K operator which is like the box
but indexed by an agent:
https://www.isa-afp.org/entries/Epistemic_Logic.html
For my master's thesis I am working on a Hybrid Logic entry which will
have the "regular" box/diamond operators, but I only started this week.
https://plato.stanford.edu/entries/logic-hybrid/
A. H. From
Email Gateway (Aug 22 2022 at 20:29):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
thank you everyone for your answers. Andreas, looking forward to your
epistemic logic entry
Best,
Angeliki
Email Gateway (Aug 22 2022 at 20:30):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Joao,
many thanks for pointing to this interesting paper
Best wishes,
Angeliki
Email Gateway (Aug 22 2022 at 20:49):From: Andreas Halkjær From <andro.from@gmail.com>
My formalization of a sound and complete tableau system for hybrid logic is
now available here:
https://bitbucket.org/isafol/isafol/src/master/Hybrid_Logic/
I am still working on it, in particular on getting rid of the Bridge rule,
but you may find it interesting already.
Best, A.
Den lør. 31. aug. 2019 kl. 15.04 skrev Dr A. Koutsoukou-Argyraki <
ak2110@cam.ac.uk>:
Last updated: Apr 25 2024 at 20:15 UTC