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

Abstract

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

Keywords

• disjunct
• resolution method
• OL-denial strategy
• finite-state grammar
• depthfirst search
• дизъюнкт
• метод резолюции
• OL-опровержение
• автоматная грамматика
• поиск в глубину
• обучение логическим моделям представления знаний