Game Logic: A Proof Transformation from Gentzen to Hilbert

Schagen, Steven J. van (2022) Game Logic: A Proof Transformation from Gentzen to Hilbert. Bachelor's Thesis, Computing Science.

Preview	Text bCS_2022_vanSchagenSJ.pdf Download (871kB) | Preview
	Text Toestemming.pdf Restricted to Registered users only Download (137kB)

Abstract

Game logic is a modal logic, introduced by Parikh in 1985, that allows to reason about determined 2- player games. It introduces the modality ⟨γ⟩φ which means that player 1, often called Angel, has a strategy in the game γ to ensure an outcome in which the formula φ holds. Parikh also came up with a proof system for game logic, a Hilbert-style system Par, but could not yet prove its completeness. In 2019, Enqvist et al. proved completeness of game logic through a sequence of proof transformations. To do so, they introduced three proof systems, of which the last one is a cut- free sequent calculus named G. The last transformation step, G to Par, was done via an intermediate Hilbert-style system called ParFull. In 2021, the transformation from CloG to G was implemented by Worthington. In 2022, an automated theorem prover (ATP) for CloG proofs was implemented by Meerholz. An ATP for CloG proofs, together with a transformation tool for CloG to G and for G to Par, proofs can be found in the CloG system and transformed into G and Par. Thus, an ATP for CloG, G and Par proofs will be effective. This thesis concerns the implementation of the transformation from G to ParFull. Using a small number of propositional tautologies that are needed to derive the rules of G in ParFull, the transformation from G to ParFull is defined. The implementation of the tool was done in Rascal and can successfully transform G proofs into ParFull proofs. Proofs in ParFull are much longer than proofs in G,

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:	03 Aug 2022 14:47
Last Modified:	03 Aug 2022 14:47
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/28264

Actions (login required)

View Item