Classical higher-order logic is suited as a meta-logic in which a range of other logics can be elegantly embedded. Interactive and automated theorem provers for higher-order logic are therefore readily applicable. By employing this approach, the automation of a variety of ambitious logics has recently been pioneered, including variants of firstorder and higher-order quantified multimodal logics and conditional logics. Moreover, the approach supports the automation of meta-level reasoning, and it sheds some new light on meta-theoretical results such as cut-elimination. Most importantly, however, the approach is relevant for practice: it has recently been successfully applied in a series of experiments in metaphysics in which higher-order theorem provers have actually contributed some new knowledge.
CITATION STYLE
Benzmüller, C. (2015). Invited talk: On a (quite) universal theorem proving approach and its application in metaphysics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9323, pp. 213–220). Springer Verlag. https://doi.org/10.1007/978-3-319-24312-2_15
Mendeley helps you to discover research relevant for your work.