Представлено стислий опис теперішнього стану системи автоматизації дедукції (САД), а також проблеми, з якими стикаються під час роботи з цією системою. Більш докладно розглянуто мовні проблеми. Система автоматизації дедукції грунтується на принципах евіденційної парадигми автоматизації математичної діяльності. На цій парадигмі базується програма "Алгоритм очевидності" (Evidence Algorithm). Система САД призначена для інтелектуальної обробки математичних текстів, такої, як автоматичне доведення теорем і верифікація текстів, записаних на ForTheL, формальній математичній мові, яка є наближеною до природної мови математичних публікацій. На сьогодні систему САД можна використовувати для встановлення вивідності секвенцій у класичній логіці першого порядку, пошуку доведень теорем у ForTheL-середовищі та верифікації замкнених ForTheL-текстів.

• Паскевич Андрій Юрійович (фізико-математичні науки)

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