Title :
On the arithmetic inexpressiveness of term rewriting systems
Author :
Vorobyov, Sergey G.
Author_Institution :
Program Syst. Inst., Acad. of Sci., Pereslavl-Zalessky, USSR
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.<>
Keywords :
Boolean functions; theorem proving; Boolean connectives; arithmetic inexpressiveness; term rewriting systems; unquantified Presburger arithmetic; Arithmetic; Computer applications; Differential equations;
Conference_Titel :
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location :
Edinburgh, UK
Print_ISBN :
0-8186-0853-6
DOI :
10.1109/LICS.1988.5120
