
TL;DR
Scroll nets are a new graph-based formalism inspired by Peirce's topological notation, enabling representation and normalization of proofs in propositional logic with potential applications in logic and computation.
Contribution
The paper introduces scroll nets, a novel formalism derived from existential graphs, with a graph-theoretic definition and a detour-elimination procedure, bridging logic and lambda calculus.
Findings
Scroll nets can simulate normalization in simply typed lambda calculus.
They provide a diagrammatic and combinatorial framework for propositional proofs.
A detour-elimination procedure analogous to cut-elimination is developed.
Abstract
We introduce a new formalism for representing proofs in propositional logic called "scroll nets". Its fundamental construct is the "scroll", a topological notation for implication proposed by C. S. Peirce at the end of the 19th century as the basis for his diagrammatic system of existential graphs (EGs). Scroll nets are derived from EGs by following the Curry-Howard methodology of internalizing inference rules inside judgments, just as terms in type theory internalize natural deduction rules. We focus on the intuitionistic implicative fragment of EGs, starting from a natural diagrammatic representation of scroll nets, and then distilling their combinatorial essence into a purely graph-theoretic definition. We also identify a notion of detour, that we use to sketch a detour-elimination procedure akin to cut-elimination. We illustrate how to simulate normalization in the simply typed…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
