Introduction Sequents, Multisets, Sets and Provability Logic Reasoning About Derivations and Derivability An Axiomatic Type Class for Multisets and Sequents Capturing the Core of Cut-Admissibility Proofs The Proof of Cut-Admissibility for GLS Conclusion

Generic Methods for Formalising Sequent Calculi Applied to Provability Logic

Jeremy Dawson and Rajeev Goré

Logic and Computation Group School of Computer Science College of Engineering and Computer Science Australian National University Canberra ACT 0200, Australia

                      http://users.rsise.anu.edu.au/~jeremy/
                        http://users.rsise.anu.edu.au/~rpg/

September 15, 2010

Outline

1 Introduction
2 Sequents, Multisets, Sets and Provability Logic
3 Reasoning About Derivations and Derivability
4 An Axiomatic Type Class for Multisets and Sequents
5 Capturing the Core of Cut-Admissibility Proofs
6 The Proof of Cut-Admissibility for GLS
7 Conclusion

Introduction

Formalisation of cut-admissibility for the GLS sequent system cut-admissibility applies for many sequent systems we try to get common elements of the proofs for re-use provability logic has unusual features (GL rule has formula on both sides of ⊢), proof more complex

We formalise the cut-elimination proof in Isabelle/HOL

Sequents and Multisets, Sets and Provability Logic

sequents Γ ⊢ Δ where Γ and Δ are “collections” of formulae Our “collections” are multisets (unordered, but repetitions counted) Tree-shaped derivations, conclusion at the bottom Tree branches where rule has > 1 premise, leaf where rule has no premises

Provability Logic Conclusion : value of the formalisation

theories very intricate, with low-level detail details can be overlooked in paper proofs, we have found bugs symbolic decision procedures (on-going work) are often very technical and complicated; no-one has verified any symbolic techniques for process calculi as far as we know: this is a first attempt it has helped us find better proofs about reduction and respectful substitutions theorem proving system helps keep track of results proved