2020/06/09 by Tiziano Dalmonte, Björn Lellmann, Dalmonte, Tiziano +5
Computer Science · #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2006.05436
openalex publication_date 2020/06/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present some hypersequent calculi for all systems of the classical cube\nand their extensions with axioms T, P, D, and, for every n\≥ 1, rule\nRD+n. The calculi are internal as they only employ the language of the\nlogic, plus additional structural connectives. We show that the calculi are\ncomplete with respect to the corresponding axiomatisation by a syntactic proof\nof cut elimination. Then we define a terminating root-first proof search\nstrategy based on the hypersequent calculi and show that it is optimal for\ncoNP-complete logics. Moreover, we obtain that from every saturated leaf of a\nfailed proof it is possible to define a countermodel of the root hypersequent\nin the bi-neighbourhood semantics, and for regular logics also in the\nrelational semantics. We finish the paper by giving a translation between\nhypersequent rule applications and derivations in a labelled system for the\nclassical cube.\n