Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq.

Rajeev Gor, Revantha Ramanayake, Ian Shillito

Browse the full TABLEAUX paper archive.