I/O Logic in HOL --- First Steps
Artificial Intelligence
2018-04-20 v2 Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.1803.09681,
title = {I/O Logic in HOL --- First Steps},
author = {Christoph Benzmüller and Xavier Parent},
journal= {arXiv preprint arXiv:1803.09681},
year = {2018}
}
Comments
7 pages, 3 figures