Description

Аннотация

В статье рассматриваются логическое исчисление позитивно-образованных формул (ПОФ-исчисление) и построенный на его основе метод автоматического доказательства теорем. ПОФ-исчисление впервые появилось в работах академиков РАН С.Н. Васильева и А.К. Жерлова в результате рассмотрения и решения задач теории управления и было описано как логический формализм первого порядка. Имеются примеры описания и решения задач теории управления, эффективно (с точки зрения выразительности языка и производительности средств доказательств теорем) решенных с помощью ПОФ-исчисления, например, управление группой лифтов, наведение телескопа на центр планеты, находящейся в неполной фазе, управление мобильным роботом. ПОФ-исчисление выгодно отличается от возможностей других, логических, средств формализации предметной области и поиска логических выводов выразительностью в сочетании с компактностью представления знаний, естественным параллелизмом их обработки, крупноблочностью и меньшей комбинаторной сложностью выводов, высокой совместимостью с эвристиками и широкими возможностями для интерактивного доказательства. В выделенном классе формул возможно построение конструктивного доказательства. Данный класс формул существенно шире класса хорновских дизъюнктов, используемых в языке Пролог: на логическую формализацию аксиоматической базы предметной области не накладываются никакие ограничения, а целевое утверждение — это конъюнкция запросов (в смысле языка Пролог). Для тестирования программной системы автоматического доказательства теорем (прувера), основанной на ПОФ-исчислении, использовалась библиотека задач TPTP (Thousands of Problems for Theorem Provers). Формат, в котором представлены задачи TPTP (называемые проблемами), де-факто стал стандартом среди сообщества, изучающего автоматизацию рассуждений. Возникает естественная необходимость в том, чтобы разрабатываемый прувер принимал на вход задачи в этом формате. Таким образом, возникла задача трансляции формул логики предикатов первого порядка, представленных в формате TPTP, в формат ПОФ. Эта задача нетривиальна из-за особой структуры формул ПОФ-исчисления. В данной работе предложены более эффективный (в сравнении с ранее разработанным алгоритмом в первой реализации системы автоматического доказательства теорем для ПОФ-исчисления) метод трансляции формул первопорядкового языка исчисления предикатов с сохранением исходной эвристической структуры знаний и его упрощенная версия для задач, представленных на языке дизъюнктов. Под эффективностью понимаются количество шагов и длина получаемых формул. Предложенный метод был реализован в виде программной системы — транслятора языка первопорядковых логических формул в формате ТРТР в язык ПОФ. Приведены результаты тестирования разработанного метода, которые позволяют сделать вывод о том, что существует определенный класс первопорядковых формул, не принимаемый во внимание как особый существующими системами автоматического доказательства теорем, в то время как в ПОФ-исчислении для данного класса формул существуют специальные стратегии, повышающие эффективность поиска вывода.The paper considers the logic calculus of positively constructed formulas (PCF calculus) and based on it automated theorem proving (ATP) method. The PCF calculus was developed and described as a first-order logic formalism in works of S.N. Vassilyev and A.K. Zherlov as a result of formalizing and solving problems of control theory. There are examples of describing and solving some control theory problems, effectively (from the point of view of the language expressiveness and the theorem proving means efficiency) solved using PCF calculus, for example, controlling a group of lifts; directing a telescope at the planet center, which is in an incomplete phase, and mobile robot control. Comparing to the capabilities of other logical means for subject domain formalization and logic conclusion search, the PCF calculus have the advantage of the expressiveness combined with the compactness of knowledge representation, the natural parallelism of their processing, large block size and lower combinatorial complexity of conclusions, high compatibility with heuristics, and great capabiliies for interactive proof. The selected class of formulas makes it possible to build constructive proofs. This class of formulas is much wider than the class of Horn clauses used in the Prolog. There are no restrictions in the logical formalization of the axiomatic base of the subject domain, and the target statement is a conjunction of queries (in terms of the Prolog). To test the ATP software system (prover) based on the PCF calculus the authors used the TPTP (Thousands of Problems for Theorem Provers) library. The TPTP format has become a standard in the community that studies automated reasoning. There is a natural need for the developed prover to accept problems in this format as input. Thus, the problem of translating the firstorder predicate logic formulas presented in the TPTP format to the POF format arises. This problem is nontrivial due to the special structure of the PCF calculus formulas. The paper proposes a more efficient translation method (compared to the previously developed algorithm in the first implementation of the prover based on the PCF calculus) for the first-order predicate calculus language preserving the original heuristic knowledge structure, and its simplified version for the problems presented in language of clauses. The efficiency is a number of steps and the length of the obtained formulas. The proposed method was implemented as a software system — a language translator of first-order TPTP logic formulas to the PCF calculus language. The paper presents test results of the developed method, which imply that there is a certain class of first-order formulas that are not taken into account as special by existing ATP systems, while the PCF calculus has special strategies that increase the efficiency of the inference search for such class of formulas.