Pytania otagowane jako automated-theorem-proving

Dowody sprawdzone maszynowo, wygenerowane maszynowo lub zweryfikowane maszynowo

1
Rodzaje automatycznych dostawców twierdzeń
Uczę się samodzielnie Automated Theorem Proving / SMT solvers / Proof Assistants i piszę serię pytań na temat tego procesu, zaczynając tutaj . Jakie są odpowiednie dowody zautomatyzowanego twierdzenia? Znalazłem Przegląd dostawców twierdzeń Czy to wciąż aktualne? Które są nadal bardzo aktywne, tj. Które są obecnie używane poza grupą, która …
2
Dlaczego niektóre silniki wnioskowania potrzebują ludzkiej pomocy, a inne nie?
Uczę się samodzielnie Automated Theorem Proving / Solver SMT / Proof Assistants i zamieszczam serię pytań na temat tego procesu, zaczynając tutaj . Dlaczego automatyczne dowodzenia twierdzeń, tj. ACL2 i solwery SMT, nie potrzebują ludzkiej pomocy, podczas gdy asystenci dowodzenia, tj. Isabelle i Coq , tak? Znajdź następne pytanie z …
1
Monadyczna logika drugiego rzędu dla manekinów
Jestem programistą z automatami, ale nie logiką. Przeczytałem w artykułach, że te dwa są ze sobą ściśle powiązane. Deterministyczne automaty skończone (DFA), automaty drzewa i automaty z widocznym przesunięciem w dół są powiązane z logiką Monadic drugiego rzędu (MSO). Chociaż rozumiem automaty i ludzie (w dokumentach) próbowali mi wyjaśnić związek …
1
Odrębne zmienne dla różnych klauzul
W dowodzeniu twierdzenia o rozdzielczości zwykle przyjmuje się, że zmienne w różnych klauzulach są różne. To nie dzieje się automatycznie; do wdrożenia wymaga znacznego dodatkowego kodu i obliczeń. Biorąc to pod uwagę, szukam dla niego skrzynki testowej. Problem polega na tym, że we wszystkich testowanych dotychczas testach nie ma to …
2
Twierdzenia Dowody w Coq
tło Uczę się pomocy, Coq, na własną rękę. Do tej pory w pośpiechu przeczytałem Coq Yvesa Bertota . Teraz moim celem jest udowodnienie podstawowych wyników dotyczących liczb naturalnych, których zwieńczeniem jest tak zwany algorytm podziału. Jednak na drodze do tego celu napotkałem pewne niepowodzenia. W szczególności dwa następujące wyniki okazały …
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.