We introduce a linear logic for contracts. The logic (called PCLLW) extends intuitionistic linear affine logic ILLW with a contractual implication connective, along the lines of Propositional Contract Logic (PCL). A proof system for PCLLW is presented, and it is shown sound and complete with respect to a phase structure model. By exploiting the finite model property, we show that PCLLW is decidable.
Towards a linear contract logic
BARTOLETTI, MASSIMO;DI GIAMBERARDINO, PAOLO;
2013-01-01
Abstract
We introduce a linear logic for contracts. The logic (called PCLLW) extends intuitionistic linear affine logic ILLW with a contractual implication connective, along the lines of Propositional Contract Logic (PCL). A proof system for PCLLW is presented, and it is shown sound and complete with respect to a phase structure model. By exploiting the finite model property, we show that PCLLW is decidable.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I metadati presenti in IRIS UNICA sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono protetti da diritto d'autore, salvo diversa indicazione.
