Model constructions for Moss' coalgebraic logic

Autor: Bergfeld, J., Venema, Y., Corradini, A., Klin, B., Cîrstea, C.
Přispěvatelé: Logic and Computation (ILLC, FNWI/FGw), ILLC (FNWI)
Jazyk: angličtina
Rok vydání: 2011
Předmět:
Zdroj: Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011: proceedings, 100-114
STARTPAGE=100;ENDPAGE=114;TITLE=Algebra and Coalgebra in Computer Science
Algebra and Coalgebra in Computer Science ISBN: 9783642229435
CALCO
Popis: We discuss two model constructions related to the coalgebraic logic introduced by Moss. Our starting point is the derivation system M T for this logic, given by Kupke, Kurz and Venema. Based on the one-step completeness of this system, we first construct a finite coalgebraic model for an arbitrary M T -consistent formula. This construction yields a simplified completeness proof for the logic M T with respect to the intended, coalgebraic semantics. Our second main result concerns a strong completeness result for M T , provided that the functor T satisfies some additional constraints. Our proof for this result is based on the construction, for an M T -consistent set of formulas A, of a coalgebraic model in which A is satisfiable.
Databáze: OpenAIRE