Javascript must be enabled for the correct page display

Towards Automated Theorem Proving in the CloG Proof System

Meerholz, Han (2021) Towards Automated Theorem Proving in the CloG Proof System. Bachelor's Thesis, Computing Science.

[img]
Preview
Text
bCS_2021_MeerholzJF.pdf

Download (1MB) | Preview
[img] 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 View Item