I/O Logic in HOL --- First Steps
This work addresses the mechanization of reasoning tasks in input/output logic for researchers and practitioners in formal logic and automated theorem proving, but it appears incremental as it builds on and corrects a previous embedding attempt.
The authors tackled the problem of automating reasoning in input/output logic by presenting a semantic embedding into classical higher-order logic, enabling the use of existing theorem provers and proof assistants.
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.