Zastanawiam się, czy ktoś może mi powiedzieć, różnica między Z3 i coq? Wydaje mi się, że coq jest asystentem dowodowym, ponieważ wymaga od użytkownika wypełnienia kroków sprawdzających, podczas gdy Z3 nie ma tego wymogu. Wygląda jednak na to, że coq ma taktykę automatyczną, która jest podobna do tego, co robi Z3? A może zdolność wyszukiwania dowodów w coq nie jest tak potężna jak Z3?Różnica między Z3 i coq
Coq to interaktywny tester twierdzeń (aka asystent dowódcy). Zapewnia język do pisania definicji matematycznych, algorytmów i twierdzeń. Zapewnia również środowisko do tworzenia proofów sprawdzanych maszynowo. Coq został użyty do sformalizowania twierdzeń matematycznych i zapewnienia semantyki języków programowania. Dziś możemy znaleźć wiele artykułów w POPL, które używały Coq. Niektórzy twierdzą, że w przyszłości systemy takie jak Coq będą szeroko stosowane przez matematyków. The article ma przekonujący argument do formalnych dowodów w matematyce. Niedawno, Georges Gonthier użył Coq do stworzenia sprawdzalnego dowodu twierdzenia o czterech kolorach. Coq ma mały zaufany rdzeń i zapewnia wysoką pewność.
Z3 jest solver w teorii spełnienia modulo SMT. Jego językiem jest wiele uporządkowanych logiki pierwszego rzędu + teorie, takie jak arytmetyczne, bitowe, typy danych, tablice itp. Ten język nie jest tak wyrazisty jak język używany w Coq. Z3 nie obsługuje również zarządzania dowodami, takimi jak Coq. Z3 jest używany głównie w testowaniu i weryfikacji oprogramowania. Może być również używany do rozwiązywania problemów, problemów związanych z planowaniem, łamigłówek itp. Istnieje ogromny nacisk na znalezienie modeli (tj. Rozwiązań) dla odpowiednich formuł. The article opisuje wiele aplikacji Z3 w Microsoft i gdziekolwiek indziej. Z3 jest zasadniczo automatycznym dowodem twierdzenia. W Z3 taktyki są używane do określenia domain specific strategies. Oznacza to, że spersonalizowane rozwiązania problemów związanych z konkretną domeną aplikacji. Z3 może produkować dowody/certyfikaty, które można niezależnie sprawdzić. Jednak generowanie dowodów nie jest głównym celem projektu Z3. Co więcej, wiele modułów nie obsługuje produkcji proofa i musi być wyłączone, gdy użytkownik żąda generowania proofa. Z3 został również zintegrowany z asystentami, takimi jak Isabelle, a niektórzy pracują nad zintegrowaniem Z3 w Coq. Chodzi o to, aby mieć najlepsze z obu światów: bardzo ekspresyjny język i bardzo dobrą automatyzację. Z3 może być również postrzegany jako silnik logicznego wnioskowania, który może być osadzony w większych aplikacjach. Właściwie tak jest w przypadku każdej aplikacji Z3. Użytkownicy końcowi nie używają bezpośrednio Z3. Jest ukryty w narzędziach takich jak Isabelle, Pex, VCC, itp. new Python front-end dla Z3 próbuje to zmienić.