# An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning

arXiv: https://arxiv.org/abs/2203.12352 · HTML: https://mlsanity.com/paper/2203.12352/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 60 references that are in the map.
- First posted on arXiv 23 Mar 2022.

## Builds on (most cited first, 3 of 3)

- [Extensional Higher-Order Paramodulation in Leo-III](https://mlsanity.com/paper/1907.11501/) (2019)
- [Automated Reasoning in Non-classical Logics in the TPTP World](https://mlsanity.com/paper/2202.09836/) (2022)
- [An Introduction to Logics of Knowledge and Belief](https://mlsanity.com/paper/1503.00806/) (2015)

## Built on by (most cited first, 4 of 4)

- [Solving Quantified Modal Logic Problems by Translation to Classical Logics](https://mlsanity.com/paper/2212.09570/) (2022)
- [Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (extended version)](https://mlsanity.com/paper/2209.05090/) (2022)
- [TPTP World Infrastructure for Non-classical Logics](https://mlsanity.com/paper/2508.09318/) (2025)
- [Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint](https://mlsanity.com/paper/2305.15382/) (2023)

## Abstract (arXiv)

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.