К автоматизации сборки механизмов с использованием автоматического доказательства теорем на примере BLOCKSWORLD

А.С. Охильков,
техн., oxil91l3v@mail.ru,
А.С. Матвеев,
техн., as.matveev@msu.physics.ru,
ИПУ РАН, г. Москва

В данной работе продемонстрирована возможность автоматизации сборки механизмов при помощи методов автоматического доказательства теорем. Процесс автоматизации в данной работе основан на применении метода представления и обработки знаний в типово-кванторном языке L позитивно-образованных формул (по-формул) с применением соответствующего первопорядкового логического исчисления J (с единственным правилом вывода ω), которое имеет ряд существенных преимуществ над другими методами [1]. Представлен пример на основе известной задачи планирования BLOCKSWORLD с дополнительными ограничениями на совместимость блоков, что является формализацией задачи о допусках и посадках.

This paper shows a possibility of automatic assembly of mechanisms with using methods of the automated theorem proving. Automation process is based on application of a method of representation and processing of knowledge in standard-quantifier language L of positive-formed formulas (pf - formulas) using the appropriate first-orderlogical calculation of J (with the single inference rule ω) which has a number of essential advantages over other methods [1]. The example on the basis of the known task of planning BLOCKSWORLD with additional restriction on compatibility of units is provided.

Введение

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

Сейчас сведётся много работ над интеллектуализацией САПР[2, 3, 4]. Одним из направлений является построение интегрированных интеллектуальных систем проектирования. Интеллектуализация САПР представляет собой усиление традиционных систем автоматизированного проектирования новыми информационными технологиями, основанными на знаниях [5]. Для повышения эффективности САПР, особенно на ранних стадиях разработки, требуется внедрить в состав их средств системы инженерии проектных знаний. Системы инженерии знаний – это программные системы, снабженные специальным инструментарием переработки трудноформализуемых сведений, включающие стратегии поиска, управление базами знаний, механизмы вывода и т.д. Эти системы на основе знаний никоим образом не подменяют обычные программные модули САПР, такие как подсистемы геометрического моделирования, пакеты программ расчетов или базы данных по конструкциям и материалам. Речь идет именно о совместном использовании интеллектуальных компонентов, основанных на знаниях, и традиционных технологий.

Следующий этап развития САПР, скорее всего, будет связан с созданием систем автоматического проектирования, которые по заданным спецификациям (техническим заданиям) будут с минимальным вмешательством человека предлагать законченные варианты проектов. Решение этих задач станет возможным, если будут найдены удовлетворительные средства формализации технических заданий и синтеза технических решений. Под синтезом технических решений подразумевается:

· нахождение дополнительных свойств объекта;

· создание порядка сборки объекта;

· расчет параметров объекта и его составляющих.

Можно предположить, что математическая логика станет основой для интеллектуальных САПР.

В данной работе представлен подход к автоматизации механосборки при помощи использования методов автоматического доказательства теорем, программная реализация которых представляет собой прувер. Пруверы - программы автоматического доказательства теорем, которые обычно используют метод резолюции или другие полные процедуры логического вывода, чаще всего основанные на принципе опровержения. Применение пруверов для автоматической сборки 3D-моделей позволит уменьшить рутинную часть разработки и проектирования в САПРах, обучающих программах и т.п.

Автоматическая механосборка

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

Процесс автоматизации в данной работе основан на применении метода представления и обработки знаний в типово-кванторном языке L позитивно-образованных формул (по-формул) с применением соответствующего первопорядкового логического исчисления J [1] (с единственным правилом вывода ω). Используется конструктивный фрагмент исчисления задач [1] вида , где Μ – произвольная спецификация средств решения задачи, записанная в языке L по-формул, а Π – спецификация цели в классе по-формул ограниченного синтаксиса (см. [1]). При этом задача в конструктивной семантике допускает сведение к классическому опровержению по-формулыG, эквивалентной конъюнкции Μ и отрицания Π [1]. Конструктивный фрагмент языка позитивно образованных формул является более выразительным, чем известные языки в других логических подходах автоматизации конструктивных действий, а именно, шире хорновского и, в частности, языка «Утопист» [6].

рис.1 Исходное и конечное состояние системы кубиков

Постановка задачи. Исходная задача представлена на рис.1.Имеются кубики, стол и манипулятор, который может брать один верхний кубик и переставлять его. Кубики имеют индекс. Независимо от индекса кубика собрать столбик «bac».На совместимость кубиков наложено ограничение. Совместимы только кубики, имеющие одинаковый индекс. Использование индексов соответствует обобщению ограничений на совместимость деталей. Введём предикаты:

· – истинен,если кубик x_i “сверху”;

· – истинен, если кубик x_iявляется кубиком;

· – истинен, если x_i лежит на y_j;

· –истинен, если x_i совместим с y_j .

Обозначим стол константой tс индексом 1.
Запишем базу знаний в виде по-формулы:
Данный фрагмент по-формулы соответствует исходному состоянию мира кубиков.
Введем правила, с помощью которых мы можем изменять состояние мира кубиков:
1. Проверяет на совместимость два кубика.
}
2.Если же два кубика совместимы, то можно поставить кубик x_mна y_m.

3.Любой кубик, если он сверху, всегда можно переставить на стол.

Целевой вопрос, содержащий False, запишем в виде:

Во втором и третьем правилах имеются предикаты, отмеченные «*». При использовании одного из этих правил атомы из базы, соответствующие данным предикатам должны удаляться, так как они «устаревают» в связи с изменением состояния мира кубиков.

При таком построении спецификация задачи, записанная в виде по-формулы, представлена формулой

(1)

Таким образом, мы имеем теорему, записанную на языке L (позитивно-образованных формул).

Особенность исчисления J в том, что оно содержит всего одно правило вывода ω. После применения некоторого количества раз правила ωв базе появятся факты, необходимые для ответа на целевой вопрос, в результате чего False сможет попасть в базу, и тогда доказательство теоремы будет закончено.Из доказательства теоремы можно синтезировать порядок выполнения действий по перестановке кубиков. Чтобы реализовать построение данного столбика “bac”, нужно спустить кубики c₁ и b₁ на стол, поставить a₁ на c₁ и потом b₁ на a₁.

1. Чтобы спустить кубики c₁ и b₁ на стол надо 2 раза воспользоваться правилом №3, тогда в базу попадут атомы ,,, , а атомы и удаляются из базы. Состояние мира кубиков изменилось, что и отразилось в базе. Теперь кубики c₁ и b₁ на столе, а те кубики, на которых они стояли стали, доступны для манипулятора.

2. Чтобы поставить a₁ на c₁ надо воспользоваться первым и вторым правилом: проверить их на совместимость и поставить один на другой. В базу попадут атомы, , ,а удалится .

3.Аналогично поставить b₁ на a₁.

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

Заключение

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

В работе показана возможность применения методов автоматического доказательства теорем для интеллектуализации САПР.

Литература

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

2. Барков, И.А. Теория конструкторской семантики / И.А. Барков. Ижевск: Изд-во ИжГТУ, 2003. -360с.

3. Колчин, А.Ф. Основные принципы разработки интеллектуальных систем проектирования / А.Ф. Колчин // Конструкторско-технологическая информатика-2000 : труды IV международного конгресса : в 2-х томах. -Том 1. – М.: Изд-во «Станкин», 2000. -С.280 – 283.

4. Mеждународный конгресс по интеллектуальным системам и информационным технологиям http://icai.tsure.ru/

5. Бутенко Д.В., Вагин В.Н., Головина Е.Ю., Еремеев А.П., Курейчик В.М., Пьявченко О.Н., Тарасов В.Б. Международная конференция «Интеллектуальные САПР-98»

6. Тыугу Э.Х. Концептуальное программирование. М.: Наука, 1984. 256 c.