Автоматичне доведення

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

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

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

Застосування[ред.ред. код]

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

Див. також[ред.ред. код]

Посилання[ред.ред. код]


Комп'ютер Це незавершена стаття про комп'ютери.
Ви можете допомогти проекту, виправивши або дописавши її.