3 papers
cs.LO2025
LISA -- A Modern Proof System
Simon Guilloud, Sankalp Gambhir, Viktor Kunčak
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof che…
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.CL2024
Byte BPE Tokenization as an Inverse string Homomorphism
Saibo Geng, Sankalp Gambhir, Chris Wendler +1
Tokenization is an important preprocessing step in the training and inference of large language models (LLMs). While there has been extensive research on the expressive power of th…