The proof of many foundational results in structural proof theory, such as the admissibility of the cut rule and the completeness of the focusing discipline, rely on permutation lemmas. It is often a tedious and error prone task to prove such lemmas as they involve many cases. This paper describes the tool Quati which is an automated tool capable of proving a wide range of inference rule permutations for a great number of proof systems. Given a proof system specification in the form of a theory in linear logic with subexponentials, Quati outputs in the permutation transformations for which it was able to prove correctness and also the possible derivations for which it was not able to do so. As illustrated in this paper, Quati's output is very similar to proof derivation figures one would normally find in a proof theory book. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Nigam, V., Reis, G., & Lima, L. (2014). Quati: An automated tool for proving permutation lemmas. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8562 LNAI, pp. 255–261). Springer Verlag. https://doi.org/10.1007/978-3-319-08587-6_18
Mendeley helps you to discover research relevant for your work.