Higher-order theorem proving and its applications
| dc.contributor.author | Steen, Alexander | |
| dc.date.accessioned | 2021-06-21T12:16:42Z | |
| dc.date.available | 2021-06-21T12:16:42Z | |
| dc.date.issued | 2019 | |
| dc.description.abstract | Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed. | en |
| dc.identifier.doi | 10.1515/itit-2019-0001 | |
| dc.identifier.pissn | 2196-7032 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/36658 | |
| dc.language.iso | en | |
| dc.publisher | De Gruyter | |
| dc.relation.ispartof | it - Information Technology: Vol. 61, No. 4 | |
| dc.subject | Theorem Proving | |
| dc.subject | Automated Reasoning | |
| dc.subject | Higher-Order Logic | |
| dc.subject | Non-Classical Logics | |
| dc.subject | Modal Logics | |
| dc.title | Higher-order theorem proving and its applications | en |
| dc.type | Text/Journal Article | |
| gi.citation.endPage | 191 | |
| gi.citation.publisherPlace | Berlin | |
| gi.citation.startPage | 187 |