Tableaux for Metainferential Logics

Abstract

The aim of this work is to introduce a series of requisites for building sound and complete tableaux systems for inferential logics based on non-deterministic valuation schemes and extend them with rules for metainferences, thus yielding metainferential tableaux system capable of proving metainferences of any level $n$. We show the construction of our tableaux for the logics of the Strong Kleene family and a wide range of different logical systems, most of which have not been studied previously from a metainferential standpoint. Furthermore, we implement this system into a user-friendly, publicly accessible software, designed both for educational purposes as well as assistance in research endeavors.