Podręcznik praktycznej logiki i zautomatyzowanego rozumowania

Opinie czytelników

Książka jest bardzo chwalona za kompleksowe i praktyczne podejście do automatycznego dowodzenia twierdzeń (ATP), w szczególności dzięki szczegółowej implementacji w OCaml. Czytelnicy doceniają przejrzystość i przyjemność pisania, choć istnieją pewne wady dotyczące jej wykorzystania jako odniesienia.

⬤ Doskonałe wprowadzenie do automatycznego dowodzenia twierdzeń z wyraźnym przejściem od podstaw do zaawansowanych tematów.
⬤ Kompletne implementacje algorytmów w OCaml, zwiększające przejrzystość i zrozumienie.
⬤ Przyjemny styl pisania, który sprawia, że temat jest wciągający.
⬤ Nadaje się do zbudowania od podstaw własnego zautomatyzowanego weryfikatora twierdzeń.
⬤ Uznawana za pozycję obowiązkową dla osób zainteresowanych zautomatyzowanymi procedurami decyzyjnymi.

⬤ Ograniczone pokrycie nowoczesnych solverów SMT.
⬤ Użycie OCaml może być postrzegane jako wada w porównaniu do bardziej powszechnie używanych języków, takich jak C++ czy Java.
⬤ Może być czasochłonne wyszukiwanie podstawowych implementacji funkcji, gdy książka jest używana jako odniesienie, a nie samouczek.

(na podstawie 5 opinii czytelników)

Oryginalny tytuł:

Handbook of Practical Logic and Automated Reasoning

Zawartość książki:

Książka ta zaspokaja zapotrzebowanie na samodzielne i szeroko zakrojone omówienie pojęć, maszyn i wykorzystania zautomatyzowanego rozumowania.

Podstawy logiki matematycznej są opisane w połączeniu z praktycznym zastosowaniem, a wszystko to przy minimalnych wymaganiach wstępnych. Podejście jest konstruktywne, konkretne i algorytmiczne: kluczową cechą jest to, że metody są opisane w odniesieniu do rzeczywistych implementacji (dla których dostarczany jest kod), z których czytelnicy mogą korzystać, modyfikować i eksperymentować.

Książka ta idealnie nadaje się dla tych, którzy szukają kompleksowego źródła informacji na temat ogólnego obszaru zautomatyzowanego rozumowania. Może być używana jako odniesienie lub jako miejsce do nauki podstaw, zarówno w połączeniu z zaawansowanymi kursami, jak i do samodzielnej nauki.