Наведено основні теоретичні відомості про формальне доведення теорем числення висловлювань і доведення теорем з детальним обґрунтуванням. Зауважено, що автоматизація пошуку доведень теорем належить до найважливіших застосувань математичної логіки. Ефективне знаходження доведень необхідне для успішного розв'язання низки задач, що виникають у сучасних інтелектуальних інформаційних системах. Такими є, зокрема, задачі подання знань і роботи з ними в базах даних і базах знань, задачі логічного програмування і дедуктивних баз даних.

• Шевельова Алла Євгенівна (фізико-математичні науки)

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"