Reference : I/O Logic in HOL --- First Steps
E-prints/Working papers : Already available on another site
Engineering, computing & technology : Computer science
Computational Sciences
http://hdl.handle.net/10993/37467
I/O Logic in HOL --- First Steps
English
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
Parent, Xavier mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
2018
CoRR
No
2331-8422
Cornell University
USA
[en] own ; Higher Order Logic ; Deontic Logic Automated Reasoning ; Universal Reasoning
[en] A semantical embedding of input/output logic in classical higher-order logic is presented. This embedding enables the mechanisation and automation of reasoning tasks in input/output logic with off-the-shelf higher-order theorem provers and proof assistants. The key idea for the solution presented here results from the analysis of an inaccurate previous embedding attempt, which we will discuss as well.
http://hdl.handle.net/10993/37467
http://arxiv.org/abs/1803.09681
https://arxiv.org/abs/1803.09681
https://arxiv.org/abs/1803.09681

There is no file associated with this reference.

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.