Proof Theory on Graphs

15 février 2021

Matteo Acclavio (Université du Luxembourg)

Exceptionnellement deux séminaires aujourd’hui : celui-ci est à 15h15.

Logic and proof theory provide methods and tools used in areas such as formal verification and model checking. However, when we model processes-as-formulas, formulas are not expressive enough: they can model only some processes, those admitting a series-parallel decomposition, but they cannot handle the more general cases.
To overcome this limitation and develop new proof-theoretical tools for process analysis, in this talk I present a proof system based on unoriented graphs instead of formulas.

After showing how this system can find applications in process analysis, I will show some basic properties of the system.