## Paper: A linear semantics for allowed logic programs (at LICS 1990)

Authors:**Cerrito, S.**

### Abstract

A declarative semantics for the class of allowed logic programs is proposed. Such a semantics is a logical theory, the linear completion of the program P, which differs from Clark's completion because the underlying logic is linear logic rather than classical logic. With respect to such a semantics, the soundness and completeness of SLDNF-resolution is proven. That is, it is proven that the computational notion of success of an allowed query Q for an allowed program P corresponds to the provability of an instantiation of Q in the linear completion of P, and the notion of failure to the provability of the (linear) negation of Q in the linear completion of P

### BibTeX

@InProceedings{Cerrito-Alinearsemanticsfor, author = {Cerrito, S.}, title = {A linear semantics for allowed logic programs}, booktitle = {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990}, year = 1990, editor = {John Mitchell}, month = {June}, pages = {219--227}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }