A Logic for Contracts
Massimo Bartoletti, Roberto Zunino · Unitn Eprints Research (Università Degli Studi di Trento) · 2009
We introduce a logic for modelling contractual committment, and study its properties. Our logic is free from modalities, and instead relies on a peculiar form of implication. In this paper, we discuss proof theory for our logic. We present a Hilbert-style axiomatisation for our logic, which is shown consistent. We also provide a Gentzen-style sequent calculus, and prove it equivalent to our axiomatization. We prove our logic decidable.