Automated Proof Search in a Cyclic Proof System for Game Logic

Worthington, Christopher (2023) Automated Proof Search in a Cyclic Proof System for Game Logic. Master's Thesis / Essay, Computing Science.

Preview	Text mCS_2023_Christopher Worthington.pdf Download (667kB) | Preview
	Text toestemming.pdf Restricted to Registered users only Download (129kB)

Abstract

This Master’s thesis aims to implement a proof search algorithm that is sound and complete relative to the Game Logic sequent calculus, CloG. The results build upon another attempt to implement proof search for CloG in a Bachelor’s thesis. In this previous thesis, an implementation was completed however there were limited concrete definitions and proofs provided. This project focuses on the theoretical definition of the algorithm by strictly defining the search space through a new altered proof system SCloG. An algorithm is implemented in the meta-programming language Rascal and is proven to be sound. An incomplete proof is given for the termination of the algorithm with a suggestion for how to prove the final condition. Partial results and observations are also given for the completeness of SCloG relative to CloG.

Item Type:	Thesis (Master's Thesis / Essay)
Supervisor name:	Hansen, H.H. and Ramanayake, D.R.S.
Degree programme:	Computing Science
Thesis type:	Master's Thesis / Essay
Language:	English
Date Deposited:	07 Aug 2023 13:45
Last Modified:	07 Aug 2023 13:45
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/31118

Actions (login required)

View Item