linlog
A linear logic solver and educational tool — still very much in its infancy.
About
A linear logic suite aimed primarily at education, in an early stage of development. The goal is a command-line program and an interactive, fully client-side website for working with linear logic sequents and proofs — inspired by Click and Collect, but with a broader feature set in mind. Contributions and feature requests are welcome; the code is licensed under the EUPL.
Planned features
- parsing and printing of sequents
- step-wise interactive sequent proving and automatic proof search (with specialized methods for sub-variants such as MLL)
- creation and verification of proof nets
- translation of classical/intuitionistic sequents into linear logic
- export of sequents, proof trees, and nets to PDF/SVG, LaTeX/Typst, plain Unicode, Rocq/Lean/Agda proofs, and an interactive web view
- further ahead: intuitionistic and affine linear logic
Architecture
Three units: a shared library (linlog-core) containing the common logic, the CLI (linlog-cli), and the web application (linlog-web). The implementation language is Rust, chosen for its performance and its strong WebAssembly support for the client-side website.