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 ![]() | |
Parent, Xavier ![]() | |
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.
All documents in ORBilu are protected by a user license.