Proof theory of modal coalgebraic logic
Project goals
As eqational logic is considered to be the logic of algebras, modal logic is the logic for coalgebras, the general concept modeling transition systéme (such as automata). The aim of the proposed project is to study modal logics developed to reason aboutcoalgebras. We concentrate on proof theoretical issues of modal logics arising in two of existing approaches to coalgebraic logic - languages arising from a logica connection, and languages based on cover modalities. Logical connection between a categoryof "spaces"(where the coalgebras live) and category of "algebras"(where the logic is studied) fixes the basic setting - what type of coalgebras are to be studied and what the propositional part of the logic should be ? and generatesa modal language automatically. Here we will study algebraic properties of the obtained modalities. A modal logic for coalgebras of type T can be based on a single cover modality with arity and semantics given by T. Here we will develop sequent proof systems in a general way. In both directions we try to generalize to categories other then Set.
Keywords
Public support
Provider
Czech Science Foundation
Programme
Post-graduate (doctorate) grants
Call for proposals
Postdoktorandské granty 11 (SGA02011GA1PD)
Main participants
—
Contest type
VS - Public tender
Contract ID
P202-11-P304
Alternative language
Project name in Czech
Teorie důkazů modální koalgebraické logiky
Annotation in Czech
Rovnicová logika je považována za logiku algeber, modální logika je logikou koalgeber ? struktur modelujících chování přechodových systémů (automatů). Navrhovaný projekt se soustředí na studium modálních logik vhodných k popisu chování koalgeber, s důrazem na jejich teorii důkazů. Zaměříme se na dva z existujících přístupů ke koalgebraické modální logice - jazyky pocházející z logické konexe, a jazyky založené na ?cover? modalitách. Logická konexe mezi kategorií prostorů (kde studujeme koalgebry) a kategorií algeber (kde definujeme logiku) ustaví, jaké koalgebry studujeme a co je výroková část zamýšlené logiky, a automaticky generuje modální jazyk. Zde budeme zkoumat algebraické vlastnosti modalit. Modální logiku koalgeber typu T lze založit na jediné?cover? modalitě, jejíž arita i sémantika je dána funktorem T. Zde obecně definujeme sekventové kalkuly. V obou případech se pokusíme výsledky generalizovat na kategorie jiné než Set.
Scientific branches
R&D category
ZV - Basic research
CEP classification - main branch
IN - Informatics
CEP - secondary branch
BA - General mathematics
CEP - another secondary branch
—
10101 - Pure mathematics
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
The project contributed with new results to the mathematical logic but the goals outlined in the proposal were not fully achieved, which can be evidenced by the number of publication outputs (two journal papers, another accepted). Still, the project results can be considered in proportion to its budget.
Solution timeline
Realization period - beginning
Jan 1, 2011
Realization period - end
Apr 13, 2015
Project status
U - Finished project
Latest support payment
Jun 6, 2013
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP16-GA0-GP-U/01:1
Data delivery date
May 6, 2016
Finance
Total approved costs
768 thou. CZK
Public financial support
768 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
768 CZK thou.
Public support
768 CZK thou.
100%
Provider
Czech Science Foundation
CEP
IN - Informatics
Solution period
01. 01. 2011 - 13. 04. 2015