LINK: A proof environment based on proof nets. LINK is a proof environment including proof nets-based provers for multiplicative linear logics: mixed linear logic, or recently called non-commutative logic (MNL), commutative linear logic (MLL) and non-commutative (or cyclic) linear logic (MCyLL). Its main characteristic is the provability analysis through automatic proof nets construction. A proof net is a particular graph-theoretic representation of proofs that appears appropriate for proof-search in MLL and MCyLL. It is a powerful alternative to deal with proof search and its problems about non-permutability and resource management. In the context of system verification, such a semantical and graphical representation of proof can be useful from a software engineering point of view. It allows to analyse provability (through proof nets) or non-provability (through proof structures that can be seen as counter-models).
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Papapanagiotou, Petros; Fleuriot, Jacques: WorkflowFM: a logic-based framework for formal process specification and composition (2017)
- Habert, L.; Notin, J.-M.; Galmiche, D.: LINK: A proof environment based on proof nets (2002)