Conference publications

Abstracts

XVIII conference

О реализации алгоритма построения вывода в исчислении секвенций

Белова Л.Ю.

Россия, 150000, г. Ярославль, ул. Советская, 14, Ярославский государственный университет им. П.Г. Демидова, каф. математической кибернетики, тел. (0852)45-8073, e-mail: luk1945@yandex.ru

В докладе [2] была намечена работа по реализации алгоритма построения вывода в исчислении высказываний. Результаты этой работы указывают на нерешённую проблему, которая особенно актуальна для разработки различных обучающих программных средств: слишком большая длина получающихся выводов и их «неестественность», то есть непохожесть на обычные приёмы математических рассуждений. Видимо, это самое уязвимое место любых подобных систем. В диалоговых обучающих системах данное обстоятельство особенно пагубно.

В связи с этим в новом варианте алгоритма за основу принято исчисление секвенций (ИС), то есть формальная теория, оперирующая с последовательностями высказываний. При этом исчисление секвенций строится на основе исчисления высказываний в аксиоматике Клини.

Такой подход позволяет сократить длину выводов и приблизить их к обычным способам математических рассуждений. За это приходится расплачиваться возросшей сложностью алгоритма: в ИС имеется 15 исходных правил вывода, к которым добавляются ещё около десятка допустимых правил – следствий, в то время как в методе резолюций, например, одно основное правило. – принцип резолюций. Но, конечно, применение того или иного метода обуславливается различием в целях программной разработки. В нашем случае интересна не эффективность, а диалоговые возможности системы.

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

Наиболее существенная часть алгоритма – определение приемлемой последовательности применения правил вывода на каждом шаге. Здесь нет доказуемой оптимальности, поэтому приходится реализовывать различные эвристические соображения.

Для обработки символьной информации удобно использовать, например, систему Wolfram-Mathematica, хотя, конечно, основная проблема – в оптимальной организации алгоритма.

Литература

1. Джексон П. Введение в экспертные системы М., СПб, Киев «Вильямс» 2002

2. Белов Ю.А., Белова Л.Ю. О процедуре построения вывода в аксиоматическом исчислении Труды XI Международной конференции "Математика, Компьютер, Образование" Пущино, 17-22 января 2005

• view as PDF