Logika a nesplnitelnost
Cíle projektu
Jak se mění délka nejkratšího důkazu daného tvrzení, když zvětšujeme složitost pojmů, jež lze v důkazu použít? Tato základní otázka logiky je pro důkazy ve slabých teoriích nebo ve výrokové logice úzce svázaná s obtížnými fundamentálními problémy výpočetní složitosti. Konkrétně, tvrzení NP/=coNP je ekvivalentní neexistenci výrokového důkazového systému, v němž mají všechny tautologie krátké důkazy. Varianty této otázky budeme studovat v rozličných důkazových systémech, které mají často kombinatorický či algebraický charakter, nebo pochází z certifikátů nesplnitelnosti dané formule produkovaných praktickými SAT algoritmy. Chceme pochopit obecnější způsoby uvažování, jež tyto systémy umožňují, v kontextu teorií prvního řádu. Cílem je získat vhled do otázek, jaké typy tvrzení je těžké nebo snadné dokázat a jaké jsou vztahy mezi důkazovými systémy. Předpokladem k této práci je hlubší porozumění schopnosti slabých logických teorií dokazovat základní matematická tvrzení.
Klíčová slova
logicproof complexitybounded arithmeticpropositional proof systemsalgebraic proof systemssearch problemsSAT solvingnonclassical logics
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
SGA0202300001
Hlavní účastníci
Matematický ústav AV ČR, v. v. i.
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
23-04825S
Alternativní jazyk
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.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
10101 - Pure mathematics
OECD FORD - vedlejší obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory
(dle převodníku)AF - Dokumentace, knihovnictví, práce s informacemi
BA - Obecná matematika
BC - Teorie a systémy řízení
BD - Teorie informace
IN - Informatika
Termíny řešení
Zahájení řešení
1. 1. 2023
Ukončení řešení
31. 12. 2025
Poslední stav řešení
K - Končící víceletý projekt
Poslední uvolnění podpory
29. 2. 2024
Dodání dat do CEP
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
CEP25-GA0-GA-R
Datum dodání záznamu
21. 2. 2025
Finance
Celkové uznané náklady
11 138 tis. Kč
Výše podpory ze státního rozpočtu
10 889 tis. Kč
Ostatní veřejné zdroje financování
249 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Uznané náklady
11 138 tis. Kč
Statní podpora
10 889 tis. Kč
0%
Poskytovatel
Grantová agentura České republiky
OECD FORD
Pure mathematics
Doba řešení
01. 01. 2023 - 31. 12. 2025