Автоматизоване доведення теорем — Вікіпедія

Автоматичне доведення (англ. 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. Процитовано.

Це незавершена стаття про інформаційні технології. Ви можете допомогти проєкту, виправивши або дописавши її.

Це незавершена стаття зі штучного інтелекту. Ви можете допомогти проєкту, виправивши або дописавши її.