3 papers
cs.LO2026
TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
Johann Rosain, Julie Cailler
The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many automated theorem provers rely on this approach, either because…
cs.LO2026
Towards Term-based Verification of Diagrammatic Equivalence
Julie Cailler, Noé Delorme, Simon Perdrix +1
A string diagram is a two-dimensional graphical representation that can be described as a one-dimensional term generated from a set of primitives using sequential and parallel comp…
cs.LO2025
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…