Further difficulties are encountered when we consider the addition of the modality! (of course) to our fragment of linear logic. We provide an elementary quantale semantics for our logic programs and give an appropriate completeness theorem. We consider a translation -- resembling those of Girard -- of the intuitionistic hereditary Harrop formulae and intuitionistic uniform proofs into our framework, and show that certain properties are preserved under this translation. We sketch the design of an interpreter for linear logic programs.

In this work we propose a labelled tableau method for ukasiewicz infinite-valued logic L . The method is based on the Kripke semantics of this logic developed by Urquhart [25] and Scott [24]. On the one hand, our method falls under the general paradigm of labelled deduction [8] and it is rather close to the tableau systems for sub-structural logics proposed in [4]. On the other hand, it provides a CoNP decision procedure for L validity by reducing the check of (...) branch closure to linear programming. (shrink)