Pytania otagowane jako proof-assistants

Aplikacje umożliwiające tworzenie formalnych dowodów. Pomagają użytkownikowi w znajdowaniu częściowych i sprawdzaniu kompletnych dowodów.

2
Definicje rekurencyjne nad typem indukcyjnym z zagnieżdżonymi komponentami
Rozważ typ indukcyjny, który ma pewne rekurencyjne zdarzenia w zagnieżdżonej, ale ściśle dodatniej lokalizacji. Na przykład drzewa ze skończonymi rozgałęzieniami z węzłami używającymi ogólnej struktury danych listy do przechowywania elementów potomnych. Inductive LTree : Set := Node : list LTree -> LTree. Naiwny sposób definiowania funkcji rekurencyjnej nad tymi drzewami …
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 …
4
Czy istnieje repozytorium dla hierarchii dowodów?
Jestem samoukiem, asystentem ds. Dowodów i postanowiłem zacząć od kilku podstawowych dowodów i podążać swoją drogą. Ponieważ dowody są oparte na innych dowodach, a zatem tworzą hierarchię, czy istnieje repozytorium hierarchii dowodów? Wiem, że mogę wybrać konkretnego asystenta proofów i przeanalizować jego bibliotekę, aby wyodrębnić jego hierarchię, jednak jeśli chcę …
1
Podejście „CPS” wyrządziło wielką szkodę wydajności w SML / NJ; uzasadnienie pożądane
W komentarzu do Nauka F #: Jakie książki w innych językach programowania można przetłumaczyć na F #, aby nauczyć się funkcjonalnych koncepcji? Makarius stwierdził: Zauważ, że podejście „CPS” wyrządziło wielką szkodę wydajności w SML / NJ. Jego model oceny fizycznej narusza zbyt wiele założeń wbudowanych w sprzęt. Jeśli weźmiesz duże …
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 …
1
Czy system typów może służyć jako asystent dowodu dla funkcji zagranicznych?
Jeśli się uwzględni: Język z bardzo ekspresyjnymi systemami typów (np. Idris ) może również mieć mechanizmy specjalne, takie jak interfejsy funkcji obcych / niebezpieczne SafePerformIO. Istnieją asystenci sprawdzania, których można użyć do udowodnienia niektórych właściwości programu napisanego w języku, który nie ma systemu typów zdolnego do wyrażania tych właściwości. Korespondencja …
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.