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.

Slides

• One slide per page

John Cowles