Автоматизоване доведення теорем

Автоматичне доведення (англ. Automated theorem proving) — доведення, реалізоване на програмному рівні. В основу покладено апарат математичної логіки. Використовуються ідеї теорії штучного інтелекту. Процес доведення базується на численні висловлень і логіці предикатів.

В силу нерозв'язності навіть достатньо простих теорій практичне застосування має лише напівавтоматичне людсько-машинне доведення. До того ж після повної автоматизації доведення називають вже обчисленням. Повністю автоматичною може бути лише перевірка доведення більш складних теорій (якщо його для цього підготувати).

Застосування

В даний час автоматичне доведення теорем на виробництві застосовується в основному при розробці і верифікації інтегральних схем. Після того, як було виявлено помилку ділення в процесорах Pentium, складні модулі операцій з рухомою комою сучасних мікропроцесорів розробляються з особливою ретельністю. У нових процесорах AMD, Intel і інших фірм автоматичне доведення теорем використовується для перевірки того, що ділення і інші операції виконуються коректно.

Див. також

• Машина висновування
• Експертна система
• Теорема про дедукцію

Посилання

• Про автоматичне доведення теорем [Архівовано 5 вересня 2019 у Wayback Machine.] (рос.)
• Система Автоматизації Дедукції (САД) [Архівовано 9 липня 2013 у Wayback Machine.] (рос.)
• SPASS: An Automated Theorem Prover for First-Order Logic with Equality [Архівовано 2 липня 2013 у Wayback Machine.] (англ.)
• Мороховець М. К. Особливості організації сучасних систем автоматизації міркувань (PDF) // Математичні машини і системи. — 2003. — Т. 2. — 1028-9763. Архівовано з джерела 4 березня 2016. Процитовано.