Logic and unsatisfiability
Project goals
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.
Keywords
logicproof complexitybounded arithmeticpropositional proof systemsalgebraic proof systemssearch problemsSAT solvingnonclassical logics
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
SGA0202300001
Main participants
Matematický ústav AV ČR, v. v. i.
Contest type
VS - Public tender
Contract ID
23-04825S
Alternative language
Project name in Czech
Logika a nesplnitelnost
Annotation in Czech
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í.
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
10101 - Pure mathematics
OECD FORD - secondary branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BA - General mathematics
BC - Theory and management systems
BD - Information theory
IN - Informatics
Solution timeline
Realization period - beginning
Jan 1, 2023
Realization period - end
Dec 31, 2025
Project status
K - Ending multi-year project
Latest support payment
Feb 29, 2024
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
CEP25-GA0-GA-R
Data delivery date
Feb 21, 2025
Finance
Total approved costs
11,138 thou. CZK
Public financial support
10,889 thou. CZK
Other public sources
249 thou. CZK
Non public and foreign sources
0 thou. CZK
Recognised costs
11 138 CZK thou.
Public support
10 889 CZK thou.
0%
Provider
Czech Science Foundation
OECD FORD
Pure mathematics
Solution period
01. 01. 2023 - 31. 12. 2025