The addition of bounded quantification and partial functions to a computational logic and its theorem prover Robert S. BoyerJ Strother Moore OriginalPaper Pages: 117 - 172
Mechanical procedure for proof construction via closed terms in typed λ calculus Marek Zaionc OriginalPaper Pages: 173 - 190
The problem of explaining the disparate performance of hyperresolution and paramodulation Larry Wos Basic Research Problem Pages: 215 - 217
Automated proofs of Löb's theorem and Gödel's two incompletensess theorems Art Quaife Problem Corner Pages: 219 - 231
