Dowodzenie twierdzeń
Stworzył pan LCF — jedno z pierwszych narzędzi do automatycznego dowodzenia twierdzeń — oraz język programowania ML do obsługi procesu dowodzenia. W jaki sposób one działały?
Robin Milner: W latach siedemdziesiątych prowadzono inne projekty związane z maszynowym dowodzeniem. Stosowano dwa ekstremalne podejścia: całkowicie automatyczne metody wyszukiwania dowodów (na przykład bazujące na słynnej zasadzie rezolucji Robinsona) lub metody całkowicie nieautomatyczne. Te drugie sprawdzały jedynie to, czy każdy składowy krok wykonywany przez człowieka jest logicznie prawidłowy (tak jak w systemie AutoMath Bruijna). Oba te podejścia wywarły istotny wpływ na stosowane współcześnie techniki dowodzenia twierdzeń.
Ja poszukiwałem rozwiązania ...
Get Wielkie umysły programowania. Jak myślą i pracują twórcy najważniejszych języków now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
