На правах рекламы:
Чистка диванов на дому спб выездная химчистка мягкой мебели диванов максиплюс.рф.
ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2018 г.)
2-летний импакт-фактор РИНЦ: 0,678
2-летний импакт-фактор РИНЦ без самоцитирования: 0,541
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 1,047
5-летний импакт-фактор РИНЦ: 0,460
5-летний импакт-фактор РИНЦ без самоцитирования: 0,389
Суммарное число цитирований журнала в РИНЦ: 7170
Пятилетний индекс Херфиндаля по цитирующим журналам: 310
Индекс Херфиндаля по организациям авторов: 412
Десятилетний индекс Хирша: 19
Место в общем рейтинге SCIENCE INDEX за 2018 год: 303
Место в рейтинге SCIENCE INDEX за 2018 год по тематике "Автоматика. Вычислительная техника": 10

Больше данных по публикационной активности нашего журнале за 2008-2018 гг. на сайте РИНЦ

Добавить в закладки

Следующий номер на сайте

2
Ожидается:
16 Июня 2020

Метод трансляции первопорядковых логических формул в позитивно-образованные формулы

The method for translating first-order logic formulas into positively constructed formulas
Дата подачи статьи: 2019-04-02
УДК: 004.021
Статья опубликована в выпуске журнала № 4 за 2019 год. [ на стр. 556-564 ]
Аннотация:В статье рассматриваются логическое исчисление позитивно-образованных формул (ПОФ-исчисление) и построенный на его основе метод автоматического доказательства теорем. ПОФ-исчисление впервые появилось в работах академиков РАН С.Н. Васильева и А.К. Жерлова в результате рассмотрения и решения задач теории управления и было описано как логический формализм первого порядка. Имеются примеры описания и решения задач теории управления, эффективно (с точки зрения выразительности языка и производительности средств доказательств теорем) решенных с помощью ПОФ-исчисления, например, управление группой лифтов, наведение телескопа на центр планеты, находящейся в неполной фазе, управление мобильным роботом. ПОФ-исчисление выгодно отличается от возможностей других, логических, средств формализации предметной области и поиска логических выводов выразительностью в сочетании с компактностью представления знаний, естественным параллелизмом их обработки, крупноблочностью и меньшей комбинаторной сложностью выводов, высокой совместимостью с эвристиками и широкими возможностями для интерактивного доказательства. В выделенном классе формул возможно построение конструктивного доказательства. Данный класс формул существенно шире класса хорновских дизъюнктов, используемых в языке Пролог: на логическую формализацию аксиоматической базы предметной области не накладываются никакие ограничения, а целевое утверждение – это конъюнкция запросов (в смысле языка Пролог). Для тестирования программной системы автоматического доказательства теорем (прувера), основанной на ПОФ-исчислении, использовалась библиотека задач TPTP (Thousands of Problems for Theorem Provers). Формат, в котором представлены задачи TPTP (называемые проблемами), де-факто стал стандартом среди сообщества, изучающего автоматизацию рассуждений. Возникает естественная необходимость в том, чтобы разрабатываемый прувер принимал на вход задачи в этом формате. Таким образом, возникла задача трансляции формул логики предикатов первого порядка, представленных в формате TPTP, в формат ПОФ. Эта задача нетривиальна из-за особой структуры формул ПОФ-исчисления. В данной работе предложены более эффективный (в сравнении с ранее разработанным алгоритмом в первой реализации системы автоматического доказательства теорем для ПОФ-исчисления) метод трансляции формул первопорядкового языка исчисления предикатов с сохранением исходной эвристической структуры знаний и его упрощенная версия для задач, представ-ленных на языке дизъюнктов. Под эффективностью понимаются количество шагов и длина получаемых формул. Предложенный метод был реализован в виде программной системы – транслятора языка первопорядковых логических формул в формате ТРТР в язык ПОФ. Приведены результа-ты тестирования разработанного метода, которые позволяют сделать вывод о том, что существует определенный класс первопорядковых формул, не принимаемый во внимание как особый существующими системами автоматического доказательства теорем, в то время как в ПОФ-исчислении для данного класса формул существуют специальные стратегии, повышающие эффективность поиска вывода.
Abstract: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 solv-ing 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 tele-scope 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 com-pactness of knowledge representation, the natural parallelism of their processing, large block size and lower combinatorial complexity of conclusions, high compatibility with heuristics, and great capabili-ties 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 re-strictions in the logical formalization of the axiomatic base of the subject domain, and the target state-ment 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 ac-cept problems in this format as input. Thus, the problem of translating the first-order 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 al-gorithm in the first implementation of the prover based on the PCF calculus) for the first-order predi-cate 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 trans-lator 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 tak-en 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.
Авторы: Давыдов А.В. (andrey.davydov@datadvance.net) - Компания «ДАТАДВАНС» (технический писатель), Москва, Россия, Ларионов А.А. (bootfrost@zoho.com) - Институт динамики систем и теории управления им. В.М. Матросова СО РАН (программист), Иркутск, Россия, Черкашин Е.А. (eugeneai@icc.ru ) - Институт динамики систем и теории управления им. В.М. Матросова СО РАН (старший научный сотрудник), Иркутск, Россия
Ключевые слова: алгоритмы трансляции, автоматическое доказательство теорем, математическая логика
Keywords: translation algorithms, automated theorem proving, mathematical logic
Количество просмотров: 1207
Статья в формате PDF
Выпуск в формате PDF (4.91Мб)

Размер шрифта:       Шрифт:

Сегодня активно развиваются автоматическое доказательство теорем (АДТ) и его приложения, о чем свидетельствуют, например, работы ежегодной конференции CADE, на секции System description которой или представляются новые системы для АДТ, или показывается развитие ранее разработанных.

В данной статье рассматриваются логиче- ское исчисление позитивно-образованных формул (ПОФ-исчисление) и построенный на его основе метод АДТ. ПОФ-исчисление выгодно отличается от возможностей других, ло- гических, средств формализации предметной области и поиска логических выводов вырази- тельностью в сочетании с компактностью представления знаний, естественным параллелизмом их обработки, крупноблочностью и меньшей комбинаторной сложностью выводов, высокой совместимостью с эвристиками и более широкими возможностями для интерактивного доказательства. В выделенном классе формул возможно построение конструктивного доказательства. Данный класс существенно шире класса хорновских дизъюнктов, используемых в Прологе: на логическую формализацию аксиоматической базы предметной области не накладывается никаких ограничений, а целевое утверждение – это конъюнкция запросов в смысле языка Пролог.

Понятие ПОФ-исчисления появилось в работах в результате описания и решения задач теории управления [1, 2]. ПОФ-исчисление описано в них как логический формализм первого порядка; приводятся примеры описания и решения задач теории управления, эффективно (с точки зрения выразительности языка и производительности средств доказательств теорем) решенных с помощью ПОФ-исчисления, например, управление группой лифтов, наведение телескопа на центр планеты, находящейся в неполной фазе, управление мобильным роботом, а также доказательства корректности и полноты исчисления.

Для тестирования программной системы АДТ [3], основанной на ПОФ-исчислении, использовалась библиотека задач TPTP (Thou­sands of Problems for Theorem Provers) [4]. Формат, в котором представлены задачи TPTP (называемые проблемами), де-факто стал стандартом среди сообщества, изучающего автоматизацию рассуждений. На сайте библиотеки TPTP представлены многие системы АДТ, например, имеющая более чем двадцатилетнюю историю система Vampire [5] или одна из новых систем Scavenger [6] и др. А в работе [7] рассматривается программа-конвертер из формата SMT-LIB в формат TPTP. Появляется естественная необходимость в том, чтобы разрабатываемый прувер принимал на вход задачи в этом формате. Таким образом, возникла не- обходимость трансляции формул логики предикатов первого порядка, представленных в формате TPTP, в формат ПОФ. Эта задача нетривиальна из-за особой структуры формул ПОФ-исчисления.

В данной работе предложен более эффективный (в сравнении с ранее разработанным алгоритмом в первой реализации системы автоматического доказательства теорем для ПОФ-исчисления [8]) метод трансляции. Под эффективностью понимаются количество шагов и длина получаемых формул. Приведены результаты тестирования разработанного метода, которые позволяют сделать вывод о том, что существует определенный класс первопорядковых формул, не принимаемый во внимание как особый системами АДТ, в то время как в ПОФ-исчислении для данного класса формул есть специальные стратегии, повышающие эффективность поиска вывода. Использование специальных стратегий вывода является перспективным направлением в области АДТ, в частности, в работе [9] приводится язык стратегий для прувера Isabelle/HOL.

Предварительные определения. Будем говорить о языке первопорядковых логических формул (ПЛФ), построенных на основе атомарных формул с помощью связок &, Ú, Ø, ®, «, кванторов ", $ и констант True, False. Понятия «терм», «атом», «литера» определяются обычным образом.

Пусть X = {x1, …, xk} – множество переменных, A = {A1, …, Am} – множество атомарных формул, F = {F1, …, Fn} – множество подформул. Тогда формулы

(("x1)…("xk)(A1 &…& Am ® (F1 Ú…ÚFn))),

(($x1) …($xk)(A1 &…& Am & (F1 &…&Fn)))

будем обозначать как "XA:F и $XA:F соответственно, имея в виду, что "-квантор соответствует ®FÚ, где FÚ означает дизъюнкцию всех подформул из F, а $-квантор соответствует ®F&, где F& означает конъюнкцию всех подформул из F.

Если F = Æ, формулы имеют вид "XA:Æ º º "XA ® False и $XA:Æ º $XA & True, так как дизъюнкция пустого количества элементов соответствует False, в то время как конъюнкция пустого количества элементов соответствует True. Будем записывать такие формулы, соответственно, "XA и $XA. Если X = Æ, тогда "A:F и $A:F также являются сокращением.

Множество атомов A называется конъюнктом. Еще раз отметим, что пустой конъюнкт эквивалентен True.

Переменные из X связаны соответствующими кванторами и называются соответственно "-переменными и $-переменными. В "XA переменные из X, которые не встречаются в конъюнкте A, называются неограниченными переменными.

Конструкции "XA и $XA называются позитивными типовыми кванторами. Поскольку A является конъюнкцией только лишь положи- тельных атомов, эту конъюнкцию также называют типовым условием для X. На практике такие конструкции обозначают, например, фразы: «для любого X, удовлетворяющего A, следует…», «существует X, удовлетворяющее условию A, такое что…» или «Для всех целых чисел x, y, z и n > 2 выполнимо xn + yn ≠ zn». Изначально термин «типовый квантор» был предложен Николя Бурбаки как часть обозначений для формализации математики, однако типовые кванторы оказались применимыми и в других областях.

Язык ПОФ

Определение ПОФ. Пусть X – множество переменных, A – конъюнкт.

· $XA и "XA называются $-ПОФ и "-ПОФ соответственно.

· Если F = {F1, …, Fn} является "-ПОФ, тогда $XA:F будет называться $-ПОФ.

· Если F = {F1, …, Fn} является $-ПОФ, тогда "XA:F будет называться "-ПОФ.

· Всякая $-ПОФ и "-ПОФ будет называться ПОФ.

Такое представление логических формул называется ПОФ, так как они записываются только с помощью позитивных типовых кванторов. Формулы не содержат знак отрицания в явном виде. Любая ПЛФ может быть представлена в виде ПОФ [2]. Таким образом, ПОФ есть особая форма записи классических формул языка предикатов подобно КНФ, ДНФ и др.

Те ПОФ, которые начинаются с "Æ, называются ПОФ в канонической форме. Любая ПОФ может быть приведена к канонической. Пусть F – это $-ПОФ, тогда формула "Æ: F º º True ® F º F. Если F – это неканоническая "-ПОФ, тогда "Æ: {$Æ: F} º True ® {True & & F} º F. Типовые кванторы "Æ и $Æ называются фиктивными, так как они не влияют на истинностное значение исходной ПОФ, а только служат конструкциями, сохраняющими корректную запись ПОФ.

Для удобства читаемости формул будем представлять их в древовидной форме. Запись QXA:{F1, …, Fn} эквивалентна

где Q – некоторый квантор. Элементы дерева называются как обычно: узел, корень, лист, ветвление и т.д. Поскольку "-кванторы соот- ветствуют дизъюнкциям подформул {F1, …, Fn}, а кванторы $ соответствуют конъюнкции, все "-узлы соответствуют дизъюнктивному ветвлению, а $-узлы конъюнктивному.

Некоторые части канонической ПОФ будем называть следующим образом:

– корень ПОФ "Æ называется корнем ПОФ;

– каждый непосредственный последователь $XA корня ПОФ называется базой; конъюнкт A называется базой фактов; ПОФ, корнем которой является база, называется базовой подформулой;

– каждый непосредственный последователь "YB базы ПОФ называется вопросом к своей базе; если вопрос является листом дерева, то он называется целевым вопросом;

– поддеревья вопросов называются консек­вентами; пустая консеквента эквивалента False.

Пример. Рассмотрим ПОФ-представление некоторой ПЛФ:

F = Ø("x$y P(x, y) ® $z P(z, z)).

Образом F в языке ПОФ является

F’=":Æ{"x:Æ{$y:P(x, y)}, "z:P(z, z){$:False}}.

Последняя ПОФ в древовидной форме имеет следующий вид:

Описание шагов метода трансляции. Метод трансляции состоит из следующих шагов.

Шаг 1. Преобразование задачи TPTP в ПЛФ. Полученная ПЛФ представляет собой отрицание конъюнкции всех формул, входящих в аннотированные формулы. Отрицание производится с той целью, что система АДТ опровергает отрицание исходной формулы, тем самым подтверждая ее доказуемость.

Шаг 2. Удаление связок ®, «, снятие двойного отрицания и применение законов де Моргана. Пусть F (возможно, с индексом) – произвольная неатомарная ПЛФ, A – атомарная ПЛФ. Тогда имеем правила преобразований (назовем эту группу преобразований Tr1), представленные в таблице 1.

Шаг 3. Уплощение конъюнкций и дизъюнкций.

Пусть ·Î{Ú, &}. Правило уплощения дизъюнкций и конъюнкций flat.

Пусть F = G1·…·Gn·C1·…·Cm, где Ci = = (Ci1·…·Ciki), тогда Fflat = G1 ·…·Gn & C11 ·… ·C1k1 ·… ·Cm1 ·… ·Cmkm.

Таблица 1

Правила преобразования Tr1

Table 1

Tr1 transformation rules

Исходная формула

Результирующая формула

1

¬¬F

FTr1

2

¬(F1 ® F2)

F1Tr1&¬F2Tr1

3

¬(F1 « F2)

(¬(F1 ® F2))Tr1Ú(¬(F2 ® F1))Tr1

4

¬(F1&…&Fn)

(¬F1)Tr1Ú…Ú(¬Fn)Tr1

5

¬(F1Ú…ÚFn)

(¬F1)Tr1&…&(¬Fn)Tr1

6

¬"XF

$X(¬F)Tr1

7

¬$XF

"X(¬F)Tr1

8

¬A

¬A

9

F1 ® F2

(¬F1)Tr1ÚF2Tr1

10

F1 « F2

(¬F1ÚF2)Tr1&(¬F2ÚF1)Tr1

11

F1&…&Fn

F1Tr1Ú…ÚFnTr1

12

F1Ú…ÚFn

F1Tr1Ú…ÚFnTr1

13

"XF

"X(F)Tr1

14

$XF

$X(F)Tr1

 

Смысл «уплощения» хорошо виден, если формулу представить синтаксическим деревом. Например, следующие требования эквивалентны:

Таблица 2Правила преобразования Tr2Table 2Tr2 transformation rules№	ПЛФ	ПОФ1	$X$YG	($X,YG)Tr22	$X

 

 

Шаг 4. Трансляция ПЛФ в ПОФ. Пусть G (возможно, с индексами) есть некоторая ПЛФ, а A (возможно, с индексами) – атомарная ПЛФ.

Введем еще одно обозначение. Пусть PQ Î {", $}, P Q, а C – некоторый конъюнкт, тогда:

Правила преобразования Tr2 можно представить в виде таблицы 2. Правило уплощения позволяет ограничить, насколько это возможно, применение правил 13 и 14, которые приводят к появлению фиктивных кванторов.

Шаг 5. Правило сокращения.

В получаемой формуле возникают узлы с фиктивными кванторами "Æ и $Æ, кроме этого, могут возникнуть излишние ветвления, плохо влияющие на дальнейший поиск логического вывода. Следующее правило позволяет максимально сократить получаемое дерево.

Если в некоторой ПОФ F

P, Q Î {", $}, P ≠ Q, C, B – конъюнкты, удовлетворяющие условию C Í B, то F эквивалентна F¢, имеющей следующий вид:

Представленное правило нуждается в доказательстве.

Пусть конъюнкт C имеет вид C1 & … & Cm. Если C Í B, то B = B¢ & C1 & … & Cm, где B¢ – некоторый, возможно, пустой конъюнкт. Переведем ПОФ F в язык исчисления предикатов. В случае, если F начинается с квантора ":

F = "xA ®(FÚ$Y(Y&B(ØCÚ$z1(D1&F1)Ú… Ú (Dk&Fk)))).

При раскрытии скобок получаем дизъюнкцию конъюнкций, одна из которых

 то есть является несущественной.

Поэтому F="xA®(FÚ$Y$Y1(B&D1&Y&F1)Ú … Ú (B&Dk&Y&Fk)), что при переводе в ПОФ-представление имеет вид, совпадающий с F¢.

Если F начинается с квантора $, то после перевода в язык исчисления предикатов получаем: F = $XA&Ф&

Распишем выражение в скобке:

Устраняем импликацию и группируем дизъюнктивные элементы в отдельную скобку:

 

Применяя закон дистрибутивности, получаем:

В первых n скобках присутствует тавтология ¬CiÚ¬Ci, поэтому

То есть

что при переводе в ПОФ-представление имеет вид, совпадающий с F¢.

Доказательство завершено.

В библиотеке TPTP, кроме задач в классическом первопорядковом представлении, достаточно большое количество задач представлено в виде множеств дизъюнктов, задачи приведены в скулемовской стандартной форме и восстановить их первоначальную формализацию проблематично. Для перевода задач, представленных в виде множеств дизъюнктов, в которых отсутствуют переменные, связанные кванторами существования, достаточно воспользоваться приведенной ниже формулой. Объединим дизъюнкты некоторого множества S в классы C1, C2, C3, C4, которые представляются следующим образом:

·  – множество единичных основных (не содержащих переменных) положительных дизъюнктов;

·  – множество положительных дизъюнктов, то есть , , где  – положительные литеры, kj > 1 – количество литер в соответствующих дизъюнктах, обозначим через  множество переменных, встречающихся в дизъюнкте ;

·  – множество отрицательных дизъюнктов, то есть   где  – положительные литеры, kj > 1 – количество литер в соответствующих дизъюнктах, обозначим через  множество переменных, встречающихся в дизъюнкте ;

·  – множество дизъюнктов, содержащих и положительные, и отрица- тельные литеры, то есть , , где  – положительные литеры, mj > 0, kj > 0 – количество отрицательных и положительных литер в соответствующих дизъюнктах, обозначим через  множество переменных, встречающихся в дизъюнкте .

ПОФ, соответствующая упорядоченному таким образом множеству дизъюнктов, будет иметь вид:

. То есть итоговая формула будет содержать n2 подформул, соответствующих дизъюнктам класса С2, n3 подформул класса С3, n4 подформул класса C4.

Тестирование. Для систем АДТ важно время, затраченное на решение задачи. Поскольку разработанный транслятор (включая синтаксический анализатор) планируется использовать в системе АДТ для ПОФ-исчисле­ния, эффективность трансляции также важна.

Эффективность работы программы в целом может зависеть от двух факторов: качества генерируемого кода компилятором (либо скорости исполнения интерпретатором) и качества используемых алгоритмов.

Важными характеристиками полученной в результате трансляции ПОФ являются количество узлов в древовидном представлении ПОФ и количество фиктивных кванторов. Поэтому процедура трансляции ПЛФ в ПОФ состоит из нескольких шагов, часть из которых направлены на уменьшение количества узлов и фиктивных кванторов. Исходная эвристическая структура ПЛФ сохраняется благодаря тому, что сохраняются кванторы " и $ и их исходный порядок следования (в отличие от процедуры скулемизации, используемой для получения КНФ, устраняющей кванторы $ и вносящей в формулы дополнительные термы).

Алгоритм трансляции написан на языке Rust [10]. Тестирование разработанных алгоритмов производилось на задачах из библиотеки TPTP. Использовался компьютер MacBookPro с процессором 2,3 GHz Intel Core i7 и оперативной памятью 8 GB 1 600 MHz DDR3.

Всего было отобрано 6 817 задач, по которым собиралась статистика. Количество задач, для которых ПЛФ-представление содержит меньше узлов, чем ПОФ-представление, равно 1 169. В таблице 3 представлены 10 таких задач. Количество задач, для которых ПОФ-представление содержит меньше узлов, чем ПЛФ-представление, равно 5 648, 10 из них приведены в таблице 4. В таблице 5 показаны 5 наиболее трудоемких для трансляции задач.

Кроме того, не обнаружено никакой зависимости между рейтингом задачи и наличием в ней неограниченных переменных в ПОФ-пред­ставлении данной задачи. Этот факт говорит о том, что для систем АДТ, основанных на методе резолюций, не имеет значения, содержит ли формализация задачи неограниченные переменные. Однако для метода АДТ, основанного на ПОФ-исчислении, отсутствие неограниченных переменных заметно улучшает эффективность поиска логического вывода. Поэтому с помощью ПОФ-исчисления естественным об- Таблица 4
Задачи, когда узлов в ПЛФ больше чем в 5 раз по сравнению с ПОФ
Table 4
The tasks with five times more nodes in first-order logic formulas comparing 
with positively constructed formulas

Задача TPTP	Узлов в ПЛФ	Связок в ПЛФ	Узлов в ПОФ	Время трансляции (сек.)
AGT024+2.p	1105	1071	182	0.0147
AGT025+2.p	1105	1071	182	0.0125
GEO301+1.p	2603	2077	516	0.0149
GEO302+1.p	2604	2078	516	0.015
GRA026+1.p	66	60	12	0.0006
LCL648+1.001.p	16	12	2	0.0007
LCL649+1.001.p	17	13	3	0.0016

Таблица 5
Наиболее трудоемкие для трансляции задачи
Table 5
The most time-consuming translation tasks

Задача TPTP	Узлов в ПЛФ	Связок в ПЛФ	Узлов в ПОФ	Время трансляции (сек.)
HWV067+1.p	356879	356875	209006	25.6
HWV061+1.p	492486	492482	251387	20.6
HWV133+1.p	2141861	2000646	4174817	19.6
SEU418+4.p	831581	655928	391496	6.78
SEU419+4.p	831605	655943	391510	6.33

разом выделяется такой особый класс формул, вывод которых можно построить быстрее, чем методом резолюций.

Заключение

В работе приводится краткое описание языка ПОФ и рассматриваются вопросы их обработки перед запуском автоматических алгоритмов поиска вывода. Представлен метод пре- образования ПЛФ в язык ПОФ в виде эффективных алгоритмов обработки первопорядковых формул.

Разработанные алгоритмы сохраняют исходную эвристическую структуру знаний, представленных формулами языка исчисления предикатов. Рассмотрены вопросы преобразования формул языка дизъюнктов в язык ПОФ, и предложен упрощенный алгоритм для трансляции таких задач.

Работа выполнялась при поддержке РФФИ, проект № 16-29-04238офи_м.

Литература

1.    Vassiliev S.N. Machine synthesis of mathematical theorems. J. Logic Program., 1990, vol. 9, no. 2–3, pp. 235–266.

2.    Васильев С.Н., Жерлов А.К., Федунов Е.А., Федосов Б.Е. Интеллектное управление динамичес­кими системами. М.: Физматлит, 2000. 352 с.

3.    Cherkashin E.A., Davydov A.V., Larionov A.A. Calculus of positively-constructed formulas, its features strategies and implementation. Proc. 36-th Intern. Convent. MIPRO 2013/CIS, Chroatia, Opatija, 2013, pp. 1289–1295.

4.    Sutcliffe G. The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0. J. Autom. Reason., 2009, vol. 43, no. 4, pp. 337–362. DOI: 10.1007/s10817-009-9143-8.

5.    Kovács L., Voronkov A. First-order theorem proving and Vampire. Proc. 25th Conf. CAV, LNCS, 2013, vol. 8044, pp. 1–35. DOI: 10.1007/978-3-642-39799-8_1.

6.    Itegulov D., Slaney J., Woltzenlogel Paleo B. Scavenger 0.1: A theorem prover based on conflict resolution. In: de Moura L. (eds.). Proc. 26th Conf. CADE, LNCS, 2017, vol. 10395, pp. 344–356. DOI: 10.1007/978-3-319-63046-5_21.

7.    Baumgartner P. SMTtoTPTP – a converter for theorem proving formats. Proc. 25th Intern. Conf. CADE, LNCS, 2015, vol. 9195, pp. 285–294.

8.    Черкашин Е.А. Программная система «КВАНТ/1» для автоматического доказательства теорем. Иркутск: Изд-во ИДСТУ СО РАН, 1999. 16 с.

9.    Nagashima Y., Kumar R. A proof strategy language and proof script generation for Isabelle/HOL. Proc. 26th Conf. CADE, LNCS, 2017, vol. 10395, pp. 528–545. DOI: 10.1007/978-3-319-63046-5_32.

10. Rust Programming Language. URL: www.rust.org (дата обращения: 25.03.2019).

References

  1. Vassiliev S.N. Machine synthesis of mathematical theorems. J. Logic Program. 1990, vol. 9, no. 2–3, pp. 235–266.
  2. Vassilyev S.N., Zherlov A.K., Fedunov E.A., Fedosov B.E. Intelligent Control of Dynamic Systems. Moscow, Fizmatlit Publ., 2000, 352 p.
  3. Cherkashin E.A., Davydov A.V., Larionov A.A. Calculus of positively constructed formulas, its features: strategies and implementation. 36th Intern. Convent. MIPRO 2013/CIS. 2013, Chroatia, Opatija, 2013, pp. 1289–1295.
  4. Sutcliffe G. The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0. J. of Automated Reasoning. 2009, vol. 43, no. 4, pp. 337–362. DOI: 10.1007/s10817-009-9143-8.
  5. Kovács L., Voronkov A. First-order theorem proving and Vampire. Proc. 25th Conf. CAV, LNCS, 2013, vol. 8044, pp. 1–35. DOI: 10.1007/978-3-642-39799-8_1.
  6. Itegulov D., Slaney J., Woltzenlogel Paleo B. Scavenger 0.1: A theorem prover based on conflict resolution. Proc. 26th Conf. CADE, LNCS. 2017, vol. 10395, pp. 344–356. DOI: 10.1007/978-3-319-63046-5_21.
  7. Baumgartner P. SMTtoTPTP – a converter for theorem proving formats. Proc. 25th Intern. Conf. CADE, LNCS. 2015, vol. 9195, pp. 285–294.
  8. Cherkashin E.A. KVANT/1 Programm System for Automated Theorem Proving. PhD Thesis. IDSTU SO RAN Publ., Irkutsk, 1999, 16 p.
  9. Nagashima Y., Kumar R. A proof strategy language and proof script generation for Isabelle/HOL. Proc. 26th Conf. CADE, LNCS, 2017, vol. 10395, pp. 528–545. DOI: 10.1007/978-3-319-63046-5_32.
  10. Rust Programming Language. Availavle at: www.rust.org (accessed March 25, 2019).

Постоянный адрес статьи:
http://swsys.ru/index.php?page=article&id=4642
Версия для печати
Выпуск в формате PDF (4.91Мб)
Статья опубликована в выпуске журнала № 4 за 2019 год. [ на стр. 556-564 ]

Назад, к списку статей