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: |
Discrete mathematics
Functor Finite model property Semantics (computer science) Coalgebra Modal logic Construct (python library) Algebra Set (abstract data type) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Completeness (logic) Mathematics::Category Theory Computer Science::Logic in Computer Science Mathematics |
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 |
Externí odkaz: |