Algebraic Methods in Proof Theory
Project goals
It is a recent trend in proof theory in non-classical logic to employ more algebraic methods and to develop the so-called algebraic proof theory. A typical example of a result in this direction is proving cut elimination in the same way that closedness w.r.t. Dedekind-MacNeille completion is proved in algebra. Other results in this direction show that current proof theory, based on Gentzen sequent calculi, works only for logics with structural axioms of low complexity. Our project aims at generalizing the current methods and thus widening the applicability of (generalized) Gentzen calculi. A related target is a study of computational complexity of nonclassical logics.
Keywords
ResiduatedLatticeResiduatedFrameGentzenCalculusCut-EliminationPromonoidalCategoryDecidabilityComputationalComplexity
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 14 (SGA02011GA-ST)
Main participants
České vysoké učení technické v Praze / Fakulta elektrotechnická
Ústav informatiky AV ČR, v. v. i.Contest type
VS - Public tender
Contract ID
P202-11-1632
Alternative language
Project name in Czech
Algebraické metody v teorii důkazů
Annotation in Czech
Jeden ze současných trendů v teorii důkazů neklasických logik je snaha zapojit více algebraických metod a vyvinout takzvanou algebraickou teorii důkazů. Typickým příkladem výsledku směřující tímto směrem je důkaz eliminace řezu stejným způsobem, jakým se v algebře dokazuje uzavřenost na Dedekind-MacNeillovo zúplnění. Další výsledky v tomto směru ukazují, že současná teorie důkazů založená na Gentzenových sekventových kalkulech funguje jen pro logiky se strukturálními axiomy nízké složitosti. Cílem našeho projektu je zobecnit současné metody za účelem rozšíření oblasti, kde lze sekventové kalkuly (v zobecněné podobě) aplikovat. S tím souvisí další cíl projektu, kterým je studium výpočetní složitosti neklasických logik.
Scientific branches
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
Many solid new results in the area of substructural logic, published in some world-top publication venues (mainly journals). The reported outcomes (incl. 3 accepted journal papers) are adequate to the size of the project and the number of researchers. The project advanced knowledge in the field of logic in CS. No important problems with following the grant rules or spending the funds were found.
Solution timeline
Realization period - beginning
Jan 1, 2011
Realization period - end
Dec 31, 2015
Project status
U - Finished project
Latest support payment
Apr 10, 2015
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-GA-U/01:1
Data delivery date
Sep 25, 2017
Finance
Total approved costs
5,771 thou. CZK
Public financial support
5,771 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Recognised costs
5 771 CZK thou.
Public support
5 771 CZK thou.
0%
Provider
Czech Science Foundation
CEP
IN - Informatics
Solution period
01. 01. 2011 - 31. 12. 2015