Zobrazeno 1 - 5
of 5
pro vyhledávání: '"Kloibhofer, Johannes"'
Autor:
Afshari, Bahareh, Kloibhofer, Johannes
We consider modal logic extended with the well-known temporal operator `eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination m
Externí odkaz:
http://arxiv.org/abs/2405.01935
Automata operating on infinite objects feature prominently in the theory of the modal $\mu$-calculus. One such application concerns the tableau games introduced by Niwi\'{n}ski & Walukiewicz, of which the winning condition for infinite plays can be n
Externí odkaz:
http://arxiv.org/abs/2307.06897
Autor:
Kloibhofer, Johannes
The system $\mathsf{Clo}$ is a cyclic, cut-free proof system for the modal $\mu$-calculus. It was introduced by Afshari & Leigh as an intermediate system in their intent to show the completeness of Kozen's axiomatisation for the modal $\mu$-calculus.
Externí odkaz:
http://arxiv.org/abs/2307.06846
Autor:
Hetzl, Stefan, Kloibhofer, Johannes
Publikováno v:
EPTCS 344, 2021, pp. 65-78
We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula equations. We state and prove a fixed-point theorem for Horn formula equ
Externí odkaz:
http://arxiv.org/abs/2109.04633
Autor:
Kloibhofer, Johannes
Formula equations are logical equations in which the unknowns are formulas. They naturally occur in many areas like program verification or automated theorem proving. In these communities similar problems are treated independently. Our motivation is
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b46e2559ec6b71aa8ccb1c559d51aba0