Logic in Computer Science (LICS 1992)

Paper: Mixing list recursion and arithmetic (at LICS 1992)

Authors: Fribourg, L.

Abstract

A procedure that constructs mechanically the appropriate lemmas for proving assertions about programs with arrays is described. A certain subclass of formulas for which the procedure is guaranteed to terminate and thus constitutes a decision procedure is exhibited. This subclass allows for ordering over integers but not for incrementation. A more general subclass that allows for incrementation, but without the termination property, is considered. It is also indicated how to apply the method to a still more general subclass that allows for full arithmetic. These results are extended to the case in which predicates have more than one list argument

BibTeX

  @InProceedings{Fribourg-Mixinglistrecursion,
    author = 	 {Fribourg, L.},
    title = 	 {Mixing list recursion and arithmetic},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {419--429},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }