Informatyka logic

1

Algorytm do tłumaczenia deterministycznego automatu Büchi na LTL (jeśli to możliwe)

Logika LTL i deterministycznych automatów BUCHI są nieporównywalne: DBA nie może wyrazić , i nie mogą wyrażać LTL „co najmniej dziwne jest każda litera«a»” . Ale czasami interesujące jest, czy język DBA może być wyrażony w LTL.FGaFGaFGa Potrzebuję algorytmu, który decyduje, czy język danego DBA można opisać w LTL. Czy …

10 logic automata linear-temporal-logic buchi-automata

2

Jaki jest obecny stan równoległych lub współbieżnych programów w izomorfizmie Curry-Howarda?

W Dowodach i typach Girarda możemy przeczytać: Z algorytmicznego punktu widzenia rachunek sekwencyjny nie ma izomorfizmu Curry'ego-Howarda ze względu na wiele sposobów pisania tego samego dowodu. To uniemożliwia nam użycie go jako maszynopisu -calculus, chociaż dostrzegamy jakąś głęboką strukturę tego rodzaju, prawdopodobnie związaną z równoległością.λλ\lambda Dowody i typy , JY …

9 reference-request logic parallel-computing

1

Sztuczka zastosowana w dowodzie podwójnie wykładniczej złożoności arytmetyki Presburger'a

Wysłałem to na MathUnderflow, ale nie otrzymałem odpowiedzi, więc pomyślałem, że spróbuję tutaj, Czytam stary artykuł Rabina i Fischera [opublikuje link, jeśli to możliwe], gdzie między innymi udowodniono podwójnie wykładniczą złożoność arytmetyki Presburger'a. Dowód opiera się na istnieniu formuły jan( x )In(x)I_{n}(x) nieformalne stwierdzenie „x <2)2)k x + 1x<22kx+1x < …

9 complexity-theory reference-request logic

2

Wprowadzenie do weryfikacji logicznej pierwszego rzędu

Próbuję nauczyć się różnych podejść do weryfikacji oprogramowania. Przeczytałem kilka artykułów. O ile się dowiedziałem, logika zdaniowa z temporalnym na ogół wykorzystuje sprawdzanie modelu za pomocą solverów SAT (w systemach trwających - reaktywnych), ale co z logiką pierwszego rzędu z temporalną? Czy wykorzystuje dowody twierdzeń? Czy może również używać SAT? …

9 reference-request logic formal-methods sat-solvers software-verification

1

Obwody o głębokości 2 z bramkami OR i MOD nie są uniwersalne?

Dobrze wiadomo, że każdą funkcję boolowską można zrealizować za pomocą obwodu boolowskiego o głębokości 2 (ponad zmiennymi, ich negacją i stałymi wartościami) zawierający bramki AND na pierwszym poziomie i jedną pojedynczą bramkę OR na górnym poziomie; jest to po prostu przedstawienie DNF z .f:{0,1}n→{0,1}f:{0,1}n→{0,1}f:\{0,1\}^n\to \{0,1\}fff Innym rodzajem bramki, która jest …

9 complexity-theory logic circuits

Pytania otagowane jako logic