ПОСТРОЕНИЕ ОБУЧАЮЩЕГО СРЕДСТВА (НА ОСНОВЕ АЛГОРИТМА ПРОВЕРКИ ПРОТИВОРЕЧИВОСТИ МНОЖЕСТВА ДИЗЪЮНКТОВ)

• Main Authors: Стась Андрей Николаевич, Карташов Денис Васильевич
• Format: Article
• Language: English
• Published: Tomsk State Pedagogical University 2017-01-01
• Series: Vestnik Tomskogo Gosudarstvennogo Pedagogičeskogo Universiteta
• Subjects: disjunct; resolution method; OL-denial strategy; finite-state grammar; depthfirst search; дизъюнкт; метод резолюции; OL-опровержение; автоматная грамматика; поиск в глубину; обучение логическим моделям представления знаний
• Online Access: http://vestnik.tspu.edu.ru/archive.html?year=2017&issue=12&article_id=6710

Рассмотрена реализация алгоритма проверки множества дизъюнктов. Используется автоматная грамматика для описания языка представления дизъюнктов, метод резолюции для проверки их противоречивости и поиск в глубину для автоматизации стратегии OL-опровержения. Данный алгоритм может применяться при автоматической проверке доказуемости или недоказуемости теоремы на основе множества некоторых аксиом. Пошаговая детализация данного алгоритма может быть использована в качестве дополнительного средства при обучении методу резолюции и поиску в пространстве состояний, а также основам формальных языков.