Pytania otagowane jako lo.logic

Logika obliczeniowa i matematyczna.

2
Jaki paradygmat automatycznego dowodzenia twierdzeń jest odpowiedni dla formalizacji w stylu Principia Mathematica?
Posiadam książkę, która zainspirowana Principia Mathematica (PM) Russella i logicznym pozytywizmem próbuje sformalizować konkretną dziedzinę, określając aksjomaty i wydając z nich twierdzenia. Krótko mówiąc, próbuje zrobić dla swojej dziedziny to, co PM próbował zrobić dla matematyki. Podobnie jak PM, został napisany, zanim możliwe było automatyczne udowodnienie twierdzenia (ATP). Próbuję przedstawić …
1
Typy W vs typy indukcyjne
Teoria typów Martina-Löfa wykorzystuje typy W do definiowania struktur indukcyjnych, takich jak liczby całkowite, listy itp. Jednak rachunek konstrukcji indukcyjnych nie używa ich w ten sam sposób, typy indukcyjne wydają się być bardziej podobne do schematów aksjomatycznych. Czy te dwa podejścia są równoważne (wydają się być)? Czy są jakieś filozoficzne …
2
Wymień wszystkie rozwiązania problemu SAT
Wszystkie znane mi solwery #SAT, np. RelSat, C2D, zwracają tylko liczbę zadowalających wystąpień. Ale chcę poznać każdy z tych przypadków? Czy istnieje taki solver #SAT lub jak powinienem zmodyfikować dostępny solver #SAT, aby to zrobić? Dziękuję Ci.
11 lo.logic  sat  software 
2
Związek twierdzeń o niekompletności Gödla z tezą Kościoła Turinga
To może być naiwne pytanie, ale proszę bardzo. (Edycja - nie ma głosów pozytywnych, ale nikt też nie odpowiedział; być może pytanie jest trudniejsze, niejasne lub niejasne, niż myślałem?) Pierwsze twierdzenie Gödela o niekompletności można udowodnić jako następstwo nierozstrzygalności problemu zatrzymania (np. Sipser Ch. 6; post na blogu Scotta Aaronsona …
1
Właściwości MSO, wykresy płaskie i niewielkie wykresy
Twierdzenie Courcelle'a stwierdza, że ​​każdą właściwość grafu definiowaną w monadycznej logice drugiego rzędu można rozstrzygać w czasie liniowym na wykresach ograniczonej szerokości . Jest to jedno z najbardziej znanych algorytmicznych meta-twierdzeń. Zmotywowany twierdzeniem Courcelle, wysunąłem następujące przypuszczenie: Przypuszczenie : Niech będzie dowolną właściwością definiowaną przez MSO. Jeśli ψ można rozwiązać …
1
Rozległość modeli rachunku lambda
Tłumaczę książkę na temat LISP i oczywiście dotyka ona niektórych elementów rachunku. Zatem wzmiankowane jest pojęcie ekstensywności wraz z niektórymi modelami λ- rachunku, a mianowicie: P ω i D ∞ (tak, z nieskończonością u góry). I mówi się, że P ω jest ekstensjonalny podczas D ∞ nie jest.λλ\lambdaλλ\lambdaP.ωPω\mathcal{P}_\omegare∞D∞D^\inftyPωPω\mathcal{P}_\omegaD∞D∞D^\infty Ale ... …
2
Odniesienia do języków programowania opartych na logice warunkowej
Logiki warunkowe to logiki, które rozszerzają tradycyjną implikację logiczną za pomocą operatorów modalnych odpowiadających innym pojęciom warunku (na przykład przyczynowy warunkowy brzmi „ powoduje„ B ”lub warunkowanie probabilistyczne „ ”, które brzmi „ dany B ”).A A | B AA□→BA◻→BA\; \square\!\!\!\!\to BAAAA|BA|BA|BAAABBB Zazwyczaj logiki te są badane teoretycznie modelowo, ale …
4
Znalezienie skończonego modelu
Wiem, że pytanie „czy formuła pierwszego rzędu ma model” jest ogólnie nierozstrzygalne.ϕϕ\phi Czy ktoś mógłby mi dać link lub książkę, która da odpowiedź na skończone modele. Jeśli mam wzór pierwszego rzędu , czy można rozstrzygnąć, czy ϕ ma model skończony? Jestem pewien, że pytanie jest dobrze znane, ale nawet nie …
1
NP vs co-NP i logika drugiego rzędu
Załóżmy, że NP = co-NP i wielomian ogranicza długość dowodu niezadowolenia dla instancji 3-CNF . Czy są więc jakieś wyniki w jakiej formie może przyjąć jakiś dowód niezadowolenia dla długości ? Tzn. Ogólnie, czy taki dowód musiałby na przykład wykorzystać pełną moc logiki drugiego rzędu nad nieskończonymi strukturami (zdaję sobie …
1
Gry Ehrenfeucht-Fraïssé (w rzeczywistości Ajtai-Fagin) dla zwykłych języków.
Immerman (Complexity opisowa, 1999) przedstawia gry EF dla egzystencjalnej monadycznej drugiego rzędu (Gry Ajtai-Fagin) na stronie 127. Jak MSO na słowach jest odpowiednikiem zwykłych języków, gra może być napisany w sposób następujący.∃∃\exists Język jest regularny tylko wtedy, gdy Delilah nie ma strategii wygranej w następującej grze: 1. Samson wybiera , …
1
P i złożoność opisowa
W zoo o złożoności napisano [ 1 ], że w złożoności opisowej można zdefiniować za pomocą trzech różnych rodzajów wzorów, który jest również , a także jako .PPPFO(LFP)FO(LFP)FO(LFP)FO(nO(1))FO(nO(1))FO(n^{O(1)})SO(HORN)SO(HORN)SO(HORN) Istnieją jednak pewne wyjątki, na przykład nie może być wyrażona przez FP (FP ma taką samą moc ekspresji z LFP). i nie …
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.