34 citations · 39 across the 12 of their papers we have counts for
12 papers
Reformalization of the Jordan Curve Theorem
Simon Guilloud, Sankalp Gambhir, Samuel Chassot
We present a case study in reformalization, a variant of autoformalization in which the input proof is not natural language but a formal development in a different proof assistant.…
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Lazar Milikic, Simon Guilloud, Khanh Nguyen +1
We present and evaluate LeanFlow, an LLM agent system specialized for translating mathematical papers into buildable Lean projects. Recent verifier-in-the-loop systems show that la…
Orthologic for SAT Solving
Vladislas de Haldat, Simon Guilloud, Viktor Kunčak
We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementati…
Are Dependent Types in Set Theory Feasible?
Yunsong Yang, Simon Guilloud, Viktor Kunčak
Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, wi…
SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
Julie Cailler, Simon Guilloud
Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an…
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…
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…
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…
Verified and Optimized Implementation of Orthologic Proof Search
Simon Guilloud, Clément Pit-Claudel
We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a…
Mechanized HOL Reasoning in Set Theory
Simon Guilloud, Sankalp Gambhir, Andrea Gilot +1
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant f…
Orthologic with Axioms
Simon Guilloud, Viktor Kuncak
We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verifi…
On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
Simon Guilloud, Viktor Kunčak
We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We us…