All
All

What are you looking for?

All
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

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