Towards a Playground for Logicians

Author: Giselle Reis

Paper Information

Title:Towards a Playground for Logicians
Authors:Giselle Reis
Proceedings:WiL Short Papers and Abstracts
Editors: Valeria de Paiva, Amy Felty and Ursula Martin
Keywords:Proof theory, Mechanized proofs, Meta-theory

ABSTRACT. Proving properties about proof systems is a necessary task to make sure that they are sound and satisfy basic criteria for the application being considered. Nevertheless, it is a tedious and error-prone task. In this talk, I will present on-going work on the development of a trustworthy system that helps with the verification of proof calculi's properties. This system allows for a natural specification of sequent-style calculi and visualization of rules in LaTeX. The user is also able to construct simple proof trees. Moreover, it can be used to check identity expansion, cut-elimination and permutation lemmas with the click of a button. Our goal is to free researchers from having to write down big and repetitive proofs, and move towards the use of mechanized proofs when meta-theory of proof systems is concerned.

Talk:Jul 08 15:00 (Session 40S)