пролог, элиминация кванторов существования

[Roman.Brodetski]

Привет!

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

Необходимо избавиться от внешнего квантора существования в формулах вида
$ \exists x (a_0\cdot x=b_o \wedge a_1\cdot x=b_1 \equiv \exists y (c\cdot x + b_1 \cdot y = e)) $

В качестве условий могут быть только линейные уравнения

Например, для формулы
$ \exists x (a\cdot x=b)$
программа должна выводить
$ (a=0 \wedge b=0)\vee(a\neq 0) $

Более сложная:
$ \exists x (a_0\cdot x=b_0 \wedge a_1\cdot x=b_1) $
$(a_0=0 \wedge b_0=0 \wedge a_1=0 \wedge b_1 = 0) \vee (a_0=0 \wedge b_0 = 0 \wedge a_1 \neq 0) \vee (a_0 \neq 0 \wedge a_1=0 \wedge b_1=0) \vee (a_0 \neq 0 \wedge a_1\cdot \frac{b_0}{a_0} = b_1)$

Если необходимо, могу привести еще несколько примеров. Понятно, что для больших формул на выходе будут получатся страшнейшие ДНФ.

Выполнить программу необходимо на одном из диалектов Пролога.

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

Мои размышления:
Необходимо хранить некую базу знаний про переменные и константы, уметь объединять базы знаний (or, and), уметь умно добавлять значения в базу. Например: в БЗ хранится информация, что $a=0$. Тогда, при попытке добавить факт $a \neq 0$, эта ветка должна обрываться. Еще, видимо, надо постоянно поддерживать ДНФ.
Необходимо обрабатывать такие ситуации:
БЗ:$ a=0,a=b $
при добавлении $b \neq 0$, ветка должна обрываться. Как это делать не совсем понятно, первое что приходит в голову - при добавлении$ a=b$ просматривать уже известные факты про а и дописывать избыточное условие $b \neq 0$. Но это едва ли хороший тон.

Для начала предлагаю обсудить алгоритм работы описанного аппарата БЗ, или предложить что-нибудь взамен.

Кто-нибудь сталкивался с подобными задачами? Есть какие-нибудь классические алгоритмы?

Заранее спасибо, надеюсь на конструктивный диалог.

-- Сб апр 09, 2011 12:40:36 --

$(\frac {a}{b}=\frac {c}{d} \wedge a=b )\Rightarrow c=d$
Это, очевидно, программа тоже должна уметь делать...