Meerholz, Han (2021) Towards Automated Theorem Proving in the CloG Proof System. Bachelor's Thesis, Computing Science.
|
Text
bCS_2021_MeerholzJF.pdf Download (1MB) | Preview |
|
Text
toestemming.pdf Restricted to Registered users only Download (127kB) |
Abstract
Game logic is a logic system used for reasoning about determined two-player games. Recently, Enqvist et al (2019) proved the completeness of game logic by making use of a circular proof system named CloG. Since CloG is a cut-free sequent system, it should be suitable for Automated Theorem Proving. To explore these automated proof search capabilities, and create an implementation of the CloG proof system, a tool has been developed in the programming language of Rascal. This thesis covers the implementation of this tool, and discusses the results of several strategies applied in this automated proof search. We found that resulting proof shapes and execution times varied based on the inputted sequent and applied strategy.
Item Type: | Thesis (Bachelor's Thesis) |
---|---|
Supervisor name: | Hansen, H.H. and Ramanayake, D.R.S. |
Degree programme: | Computing Science |
Thesis type: | Bachelor's Thesis |
Language: | English |
Date Deposited: | 16 Aug 2022 09:06 |
Last Modified: | 16 Aug 2022 09:06 |
URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/28388 |
Actions (login required)
View Item |