For more information about this meeting, contact Stephen Simpson.
|Title:||Translating computer programs into the predicate calculus|
|Speaker:||Stephen G. Simpson, Pennsylvania State University|
|We briefly review the register machine model of computation. We show how to associate to each register machine program P a sentence A_P of the predicate calculus, such that P halts if and only if A_P is logically valid. From this we deduce Church's Theorem: the problem of logical validity for sentences of the predicate calculus is algorithmically unsolvable. If time permits, we shall also deduce Trakhtenbrot's Theorem concerning validity in finite structures.|
Room Reservation Information
|Room Number:||309 Boucke Building|
|Date:||09 / 09 / 2008|
|Time:||02:30pm - 03:45pm|