3 papers
cs.CL2025
RLMEval: Evaluating Research-Level Neural Theorem Proving
Auguste Poiroux, Antoine Bosselut, Viktor Kunčak
Despite impressive results on curated benchmarks, the practical impact of large language models (LLMs) on research-level neural theorem proving and proof autoformalization is still…
cs.LO2025
Interpolation and Quantifiers in Ortholattices
Simon Guilloud, Sankalp Gambhir, Viktor Kunčak
We study quantifiers and interpolation properties in \emph{orthologic}, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical…
cs.PL2025
Orthologic Type Systems
Simon Guilloud, Viktor Kunčak
We propose to use orthologic as the basis for designing type systems supporting intersection, union, and negation types in the presence of subtyping assumptions. We show how to ext…