Logic in Computer Science (LICS 1990)

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}
  }