In automated reasoning, there is a perceived trade-off between expressiveness and automation. Higher-order logic is typically viewed as expressive but resistant to automation, in contrast with firstorder logic and its fragments. We argue that higher-order logic and its variants actually achieve a happy medium between expressiveness and automation, particularly when used as a front-end to a wide range of decision procedures and deductive procedures. We illustrate the discussion with examples from PVS, but some of the observations apply to other variants of higher-order logic as well.
CITATION STYLE
Shankar, N. (2001). Using decision procedures with a higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 5–26). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_3
Mendeley helps you to discover research relevant for your work.