Some obstacles to the automation of reasoning, and the problem of redundant information Larry Wos Basic Research Problem Pages: 81 - 90
A case study in automated theorem proving: Finding sages in combinatory logic William McCuneLarry Wos Problem Corner Pages: 91 - 107