Department of Computer Sciences

1999 ACL2 Workshop

March 29 - March 31, 1999

Knuth's Generalization of McCarthy's 91 Function

Donald E. Knuth of Stanford University asks for a ``proof by computer'' of a theorem about his generalization, involving REAL parameters, of McCarthy's 91 function. This talk explores a largely successful attempt to use ACL2 to meet Knuth's challenge. The REALness of the parameters is dealt with by mechanically verifying results that are true, not only about the REALs, but also about every subfield of the REALs.


John Cowles

Last updated March 1999
Computer Sciences Department
University of Texas at Austin