Most current research on automated theorem proving is concerned with proving theorems of first-order logic. We discuss two examples which illustrate the advantages of using higher-order logic in certain contexts. For some purposes type theory is a much more convenient vehicle for formalizing mathematics than axiomatic set theory. Even theorems of first-order logic can sometimes be proven more expeditiously in higher-order logic than in first-order logic. We also note the need to develop automatic theorem-proving methods which may produce proofs which do not have the subformula property.
CITATION STYLE
Andrews, P. B., & Bishop, M. (1996). On sets, types, fixed points, and checkerboards. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1071, pp. 1–15). Springer Verlag. https://doi.org/10.1007/3-540-61208-4_1
Mendeley helps you to discover research relevant for your work.