Автоматизоване доведення теорем
Автоматичне доведення (англ. 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. Процитовано.
 | Це незавершена стаття про інформаційні технології. Ви можете допомогти проєкту, виправивши або дописавши її. |
 | Це незавершена стаття зі штучного інтелекту. Ви можете допомогти проєкту, виправивши або дописавши її. |