Ordinal Arithmetic with List Structures

@inproceedings{citeulike:1512221, abstract = {We provide a set of \"natural\" requirements for well-orderings of (binary) list structures. We show that the resultant order-type is the successor of the first critical epsilon number. The checker has to verify that the process comes to an end. Here again he should be assisted by the programmer giving a further definite assertion to be verified. This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops. To the pure mathematician it is...}, author = {Dershowitz, Nachum and Reingold, Edward M. }, booktitle = {Logical Foundations of Computer Science}, citeulike-article-id = {1512221}, keywords = {arithmetic, ordinals}, pages = {117--126}, posted-at = {2007-07-30 06:48:31}, priority = {0}, title = {Ordinal Arithmetic with List Structures}, url = {http://citeseer.ist.psu.edu/168717.html}, year = {1992} }

TY - CONF ID - citeulike:1512221 L3 - citeulike-article-id:1512221 TI - Ordinal Arithmetic with List Structures T2 - Logical Foundations of Computer Science SP - 117 EP - 126 N2 - We provide a set of "natural" requirements for well-orderings of (binary) list structures. We show that the resultant order-type is the successor of the first critical epsilon number. The checker has to verify that the process comes to an end. Here again he should be assisted by the programmer giving a further definite assertion to be verified. This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops. To the pure mathematician it is... KW - arithmetic KW - ordinals AU - Dershowitz, Nachum AU - Reingold, Edward PY - 1992/// UR - http://citeseer.ist.psu.edu/168717.html ER -