Paper: On the arithmetic inexpressiveness of term rewriting systems (at LICS 1988)

Authors: Sergei G. Vorobyov

Abstract

Unquantified Presburger arithmetic is proved to be nonaxiomatizable by a canonical (i.e. Noetherian and confluent) term-rewriting system, if Boolean connectives are not allowed in the left-hand sides of the rewrite rules. It is conjectured that the same is true if the number of Boolean connectives in left-hand sides of the rules is uniformly bounded by an arbitrary natural number

BibTeX

  @InProceedings{Vorobyov-Onthearithmeticinex,
    author = 	 {Sergei G. Vorobyov},
    title = 	 {On the arithmetic inexpressiveness of term rewriting systems},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {212--217},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }