Logika a nesplnitelnost

Název projektu anglicky
Logic and unsatisfiability
Anotace anglicky
How does the size of the smallest proof of a statement change, as we increase the complexity of the concepts used in the proof? This is a basic question in logic which, for proofs in weak theories or in propositional logic, is tied to fundamental difficult issues in computational complexity. In particular, showing that NP/=coNP is equivalent to showing that there is no propositional proof system which has short refutations of every contradiction. We will study variations of this question for a range of proof systems. These often have a combinatorial or algebraic nature, or can arise from certificates that a formula is unsatisfiable, produced by a practical SAT solver. We will make progress by understanding, in terms of first-order logic, the high-level kinds of reasoning captured by these systems, to gain insight into which kinds of statements are hard or easy for them and into the relationships between different systems. A foundation for this work is a good understanding of the strength of weak logical theories in proving basic mathematical statements.

Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
10101 - Pure mathematics
OECD FORD - vedlejší obor
—
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)
BA - Obecná matematika

Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP23-GA0-GA-R
Datum dodání záznamu
17. 3. 2023

Podobné projekty(10)