An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
This work addresses the challenge of automated reasoning for non-classical logics, which is incremental as it builds on existing theorem-proving methods.
The paper tackles the problem of automating reasoning for non-classical logics by developing an extensible tool that encodes these problems into classical higher-order logic, enabling the use of existing theorem provers for logics with limited or no automation.
The logic embedding tool provides a procedural encoding for non-classical reasoning problems into classical higher-order logic. It is extensible and can support an increasing number of different non-classical logics as reasoning targets. When used as a pre-processor or library for higher-order theorem provers, the tool admits off-the-shelf automation for logics for which otherwise few to none provers are currently available.