Formalization of the BI sequent calculus and an algebraic/semantic proof of cut elimination. WIP
-
Notifications
You must be signed in to change notification settings - Fork 1
Cut elimination for the logic of Bunched Implications (BI), and some extensions.
License
co-dan/BI-cutelim
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
About
Cut elimination for the logic of Bunched Implications (BI), and some extensions.