Proof Transformations for Game Logic

Worthington, Christopher (2021) Proof Transformations for Game Logic. Bachelor's Thesis, Computing Science.

Preview	Text bCS_2021_CWorthington.pdf Download (3MB) | Preview
	Text Toestemming.pdf Restricted to Registered users only Download (92kB)

Abstract

This bachelor thesis will cover the implementation of a tool to perform a proof transformation from one proof system to another in game logic. Game logic is a logic introduced by Rohit Parikh for reasoning about two-player determined games. The proof systems and transformation were introduced in a recent game logic completeness paper. The two proof systems, named CloG and G, are sequent calculi that use different axioms and inference rules to prove propositions in game logic. The tool successfully allows the user to input a proof of a proposition in CloG and retrieve a proof for the same proposition in G. The reason for this transformation is to investigate the relation between proofs in CloG and G when using this transformation and, due to there existing an efficient proof search for CloG, to perhaps be used in a proof search for G. The metaprogramming language Rascal is used to implement the transformation as its tools for using abstract syntax trees are well suited to handling proof trees and game logic expressions.

Item Type:	Thesis (Bachelor's Thesis)
Supervisor name:	Hansen, H.H. and Storm, T. van der
Degree programme:	Computing Science
Thesis type:	Bachelor's Thesis
Language:	English
Date Deposited:	13 Aug 2021 05:55
Last Modified:	13 Aug 2021 05:55
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/25673

Actions (login required)

View Item