Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
A logic for contracts
@TECHREPORT{BZ09d,
title = {{A logic for contracts}},
author = {{Massimo} {Bartoletti} and {Roberto} {Zunino}},
note = {Technical Report DISI-09-034},
abstract = {We investigate the logical foundations of contracts in distributed applications. A contract is an agreement stipulated between two or more parties, which specifies the duties and the rights of the parties involved therein. We model contracts as formulae in an intuitionistic logic extended with a “contractual” form of implication \coimp. This supports for a variant of Modus Ponens, where from a “promise” a\coimp b to deduce b, one does not need to know a; yet, it suffices to have a dual promise b\coimp a. We study the proof theory for our logic. In particular, we provide it with a Hilbert-style axiomatisation, which is shown consistent, and with a Gentzen-style sequent calculus, shown equivalent to the axiomatization. We prove our logic decidable, via a cut elimination property. The rights and the duties deriving from any set of contracts can therefore be mechanically inferred.},
year = {2009},
url = {http://people.unica.it/bart/files/2009/11/contract-logic.pdf},
keywords = {compliance},
partner = {UNITN},
task = {T3.5, T5.1},
}
|
