Papers for

proof assistant implementers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Framework captures complex multi-output logical reasoning with graph structures

A Fibrational Framework For Multi-Conclusion Logics

Abstract: The fibrational framework of Licata, Shulman, and Riley gives a uniform account of substructural and modal logics for single-conclusion judgments. This thesis extends it to a multiple-output setting in which cartesian resources may be used freely, while linear resources occur exactly once on either side of the turnstile. Judgments are indexed by descriptors: directed acyclic graphs generalizing the tree-shaped expressions of the original framework. Descriptor $2$-cells encode structural transformations, and explicit gates provide weakening, contraction, coweakening, and cocontraction at linear modes. We define a sequent calculus generated by two connectives, $F$ and $U$. We prove identity, invertibility, and cut admissibility. The mode and type theories present linear-non-linear $2$-polycategories, and the projection is a local discrete fibration and a fibration, with opcartesian lifts for one-output base morphisms. Two adequacy results validate the framework: its cartesian fragment recovers the Licata--Shulman--Riley calculus, and its purely linear fragment presents classical multiplicative linear logic. Finally, we relate indexed and fibrational semantics. After developing representability correspondences for multicategories and polycategories, we establish an equivalence between multi-indexed categories over a fixed representable base and multicategorical opfibrations over it, together with its biclosed bifibrational version. We also give a one-way construction from planar poly-indexed data to a planar polycategory.

Tue 27 OctLogic in Computer Science
The gist
Logical systems often use trees to represent reasoning with single conclusions. This work by the authors expands this to handle multiple conclusions by using graphs instead of trees, allowing for more complex reasoning patterns. They develop rules and prove important properties like how to combine and simplify reasoning steps. Their framework links to known logical systems and offers new ways to understand logical reasoning structures through advanced category theory concepts.
Open → 2610.36552v1