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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

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

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

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

[ред. | ред. код]

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

Див. також

[ред. | ред. код]


Посилання

[ред. | ред. код]