Używasz złożoności Kołmogorowa, aby ustalić dolne granice złożoności dowodu?

11

Motywacją tego pytania jest fakt, że większość ciągów n-bitowych jest nieściśliwa. Intuicyjnie możemy zaproponować przez analogię, że większość dowodów dla tautologii jest nieściśliwa dla wielkości wielomianowej. Zasadniczo, moja intuicja jest taka, że ​​niektóre dowody są z natury losowe i nie można ich skompresować.

Czy istnieje dobre odniesienie do wysiłków badawczych związanych z wykorzystaniem wyników złożoności Kołmogorowa do ustalenia super-wielomianowych dolnych granic dowodu wielkości tautologii?

W tym doktoracie rozprawa na temat złożoności systemów dowodu dowodowego metoda nieściśliwości złożoności Kołmogorowa służy do uzyskania dolnej granicy Urquharta dla klasy Tautologii. Zastanawiam się, czy są lepsze wyniki przy użyciu metody nieściśliwości czy inne wyniki ze złożoności Kołmogorowa?Ω(n/logn)

Mohammad Al-Turkistany
źródło
4
Złożoność Kołmogorowa nie wydaje się przydatna w tautologiach. W każdym systemie formalnym dowód leksykograficzny, że formuła bitowa jest tautologią, jest w rzeczywistości niezwykle ściśliwy: można ją opisać bitami , określając formułę wraz z programem, który wypróbowuje wszystkie dowody w jakiś system formalny w porządku leksykograficznym. Bardziej sensowne byłoby przyjrzenie się ograniczonym czasowo wersjom złożoności Kołmogorowa. n + O ( 1 )nn+O(1)
Ryan Williams,
Nie byłem jasny, mam na myśli wyniki złożoności Kołmogorowa. Pytanie jest edytowane.
Mohammad Al-Turkistany,
3
Komentarz Ryana jest nadal odpowiedni, nawet po edycji. O ile nie związałeś jakiegoś zasobu, złożoność Kołmogorowa dowolnego dowodu jest stała (dla ustalonego licznika dowodu siły brutalnej) plus rozmiar zdania. W ten sposób nie można uzyskać lepszych dolnych granic niż liniowy.
András Salamon,
2
Twoje pytanie dotyczy konkretnie „super-wielomianowych dolnych granic”. Argument Ryana pokazuje, że odpowiedź jest trywialnie przecząca, ponieważ złożoność Kołmogorowa jest co najwyżej liniowa. Dolna granica Galesi jest podliniowa, nie mówiąc już o superpolinomii.
András Salamon,

Odpowiedzi:

1

Arvind, Köbler, Mundhenk i Torán wprowadzili pojęcie ograniczonej czasowo niedeterministycznej złożoności instancji. Na podstawie szybkiego czytania wydaje się, że używają miary złożoności Kołmogorowa, która zależy od wielkości najkrótszej niedeterministycznej TM. Udało im się udowodnić istnienie trudnych do udowodnienia tautologii pod pojęciem twardości opartej na niedeterministycznej złożoności instancji.

Vikraman Arvind, Johannes Köbler, Martin Mundhenk, Jacobo Torán, niedeterministyczna instancja złożoności i trudne do udowodnienia tautologie,

Mohammad Al-Turkistany
źródło