An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning

TL;DR

This paper introduces an extensible tool that encodes various non-classical logics into classical higher-order logic, enabling automated reasoning with minimal additional prover support.

Contribution

It presents a novel, flexible encoding tool that supports multiple non-classical logics within higher-order theorem provers, enhancing automation and applicability.

Findings

Supports an increasing range of non-classical logics

Enables off-the-shelf automation for complex reasoning tasks

Facilitates integration with existing higher-order theorem provers

Abstract

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.