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 1 article , 1 standard article )
Showing result 1 of 1.