论文标题
轻质非经典推理的可扩展逻辑嵌入工具
An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
论文作者
论文摘要
逻辑嵌入工具为经典的高阶逻辑提供了一个程序编码，以将非经典的推理问题进行编码。它是可扩展的，可以支持越来越多的不同古典逻辑作为推理目标。当用作高阶定理掠夺的预处理器或库时，该工具可以接受逻辑的现成自动化，否则当前很少有掠夺。
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.
