paper-with-me

홈 › Papers

An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning

2022-03-23 · Alexander Steen

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.

📄 PDF Abstract BibTeX arXiv:2203.12352

Code (1)

leoprover/logic-embedding 공식 구현

Similar Papers 제목 키워드 기반

Leveraging Foundation Models for Histological Grading in Cutaneous Squamous Cell Carcinoma using PathFMTools

2025-11-24 · Abdul Rahman Diab, Emily E. Karn, Renchin Wu, Emily S. Ruiz 외 arxiv

Despite the promise of computational pathology foundation models, adapting them to specific clinical tasks remains challenging due to the complexity of whole-slide image (WSI) processing, the opacity of learned features,…

Faithful Logic Embeddings in HOL -- Deep and Shallow

2025-02-26 · Christoph Benzmüller

Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous …

AllAutomated Theorem Proving

Bridging Semantics and Physical Execution: A Neuro-Symbolic Framework for Multi-Pair Robotic Assembly

2026-06-09 · Xinyi Li, Aiguo Song, Linhu Wei, Huijun Li arxiv

Multi-pair robotic assembly in unstructured environments faces spatial interference and contact uncertainties. Existing paradigms fail to bridge cognitive decision-making and physical execution, as they either encounter …

Systematic Verification of the Modal Logic Cube in Isabelle/HOL

2015-07-31 · Christoph Benzmüller, Maximilian Claus, Nik Sultana

We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this prob…

QueryGym: A Toolkit for Reproducible LLM-Based Query Reformulation

2025-11-20 · Amin Bigdeli, Radin Hamidi Rad, Mert Incesu, Negar Arabzadeh 외 arxiv

We present QueryGym, a lightweight, extensible Python toolkit that supports large language model (LLM)-based query reformulation. This is an important tool development since recent work on llm-based query reformulation h…