Back to Search
Start Over
Functorial Coalgebraic Logic: The Case of Many-sorted Varieties.
- Source :
- ENTCS: Electronic Notes in Theoretical Computer Science; Jun2008, Vol. 203 Issue 5, p175-194, 20p
- Publication Year :
- 2008
-
Abstract
- Abstract: Following earlier work, a modal logic for T-coalgebras is a functor L on a suitable variety. Syntax and proof system of the logic are given by presentations of the functor. This paper makes two contributions. First, a previous result characterizing those functors that have presentations is generalized from endofunctors on one-sorted varieties to functors between many-sorted varieties. This yields an equational logic for the presheaf semantics of higher-order abstract syntax. As another application, we show how the move to functors between many-sorted varieties allows to modularly combine syntax and proof systems of different logics. Second, we show how to associate to any set-functor T a complete (finitary) logic L consisting of modal operators and Boolean connectives. [Copyright &y& Elsevier]
- Subjects :
- FUNCTOR theory
ALGEBRA
LOGIC
PROOF theory
MATHEMATICAL logic
Subjects
Details
- Language :
- English
- ISSN :
- 15710661
- Volume :
- 203
- Issue :
- 5
- Database :
- Supplemental Index
- Journal :
- ENTCS: Electronic Notes in Theoretical Computer Science
- Publication Type :
- Periodical
- Accession number :
- 32557122
- Full Text :
- https://doi.org/10.1016/j.entcs.2008.05.025