摘要：Рассмотрена реализация алгоритма проверки множества дизъюнктов. Используется автоматная граммати- ка для описания языка представления дизъюнктов, метод резолюции для проверки их противоречивости и по- иск в глубину для автоматизации стратегии OL-опровержения. Данный алгоритм может применяться при авто- матической проверке доказуемости или недоказуемости теоремы на основе множества некоторых аксиом. По- шаговая детализация данного алгоритма может быть использована в качестве дополнительного средства при обучении методу резолюции и поиску в пространстве состояний, а также основам формальных языков.
其他摘要：The use of knowledge-based algorithms is one of the most relevant directions. Often these algorithms are referred to as intelligent. It is accepted to distinguish four main classes of such models: logical, productional, frame-based, and network. As we know, the use of any given models is driven by the tasks in hand. From this perspective, logical models have gained momentum. In particular, these models are often used in the creation of expert systems and the automation of proofs of theorems. This article discusses how to implement the validation algorithm for multiple disjuncts. An automatic grammar is used to describe the language of presenting the disjuncts, a resolution method to check their inconsistencies, and a depthfirst search to automate the OL-denial strategy. This algorithm can be used to automatically check provability or indefeasibility of theorems based on many axioms. The step-by-step detalization of this algorithm can be used as an additional tool for teaching the resolution method and searching the state space as well as the basics of the formal languages. The type of going around state space depends on the order of the points in the list OPEN. When searching in the first point’s depth to open it you select the point that is most remote from the intentional one. In this case, you can simplify the implementation of this method by applying a recursive subprogram.
关键词：дизъюнкт;метод резолюции;OL-опровержение;автоматная грамматика;поиск в глу-бину;обучение логическим моделям представления знаний
