I/O Logic in HOL --- First Steps

Reference : I/O Logic in HOL --- First Steps


	Document type :	E-prints/Working papers : Already available on another site
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Computational Sciences
	To cite this reference:	http://hdl.handle.net/10993/37467

Title :	I/O Logic in HOL --- First Steps
Language :	English
Author, co-author :	Benzmüller, Christoph [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
	Parent, Xavier [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
Publication date :	2018
Publisher :	CoRR
Peer reviewed :	No
ISSN :	2331-8422
City :	Cornell University
Country :	USA
Keywords :	[en] own ; Higher Order Logic ; Deontic Logic Automated Reasoning ; Universal Reasoning
Abstract :	[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.
Permalink :	http://hdl.handle.net/10993/37467
Other URL :	http://arxiv.org/abs/1803.09681
Commentary :	https://arxiv.org/abs/1803.09681
source URL :	https://arxiv.org/abs/1803.09681

There is no file associated with this reference.

All documents in ORBi^lu are protected by a user license.