Graph-based Logic and Sketches
Atish Bagchi, Charles Wells

TL;DR
This paper introduces forms, a generalization of sketches for specifying mathematical structures in categories, and proposes a novel graph-based logic for formal reasoning within this framework.
Contribution
It extends the concept of sketches to forms, enabling the specification of complex structures, and develops a new graph-based logic for categorical assertions and proofs.
Findings
Forms can specify a wider range of structures than traditional sketches
A new graph-based logic provides an intrinsic categorical foundation for assertions and proofs
Detailed relationship between multisorted equational logic and finite product theories
Abstract
We present the basic ideas of forms (a generalization of Ehresmann's sketches) and their theories and models, more explicitly than in previous expositions. Forms provide the ability to specify mathematical structures and data types in any appropriate category, including many types of structures (e.g. function spaces) that cannot be specified by sketches. We also outline a new kind of formal logic (based on graphs instead of strings of symbols) that gives an intrinsically categorial definition of assertion and proof for each type of form. This formal logic is new to this monograph. The relationship between multisorted equational logic and finite product theories is worked out in detail.
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.
Taxonomy
TopicsData Visualization and Analytics · Topological and Geometric Data Analysis · Constraint Satisfaction and Optimization
