14.3. Формализация

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

14.3.1. Формулы, получаемые по первичной схеме ситуаций

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

(кликните для просмотра скана)

выражениями Низкое) давление (точка, Высокое), (3 насос) [скорость (насос, Высокая) скорость (насос, Низкая), (3 станция) уровень (станция, Низкий).

Из овальных вершин, помеченных этими выражениями, ведут дуги в прямоугольные вершины, помеченные соответственно действиями

Из этих вершин дуги ведут в вершины ситуаций Это означает, что истинность формул в овальных вершинах влечет истинность соответствующих действий, а истинность действий — переход в соответствующие ситуации. Следовательно, имеем формулы

14.3.2. Формулы регулирования давления в контрольных точках

На схеме регулирования давления в контрольных точках (рис. 14.5) из ситуации 5, выходят две дуги, направленные в овальные вершины, которые помечены соответственно формулами

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

Это означает, что истинность формулы (14.1) в ситуации St влечет истинность формулы (14.3), а истинность формулы (14.2) влечет истинность формулы (14. 4) в этой же ситуации. Следовательно, имеем формулы

Из прямоугольных вершин, соответствующих действиям (14.3), (14.4), дуги ведут вновь в ситуацию 5,. Следовательно, имеем формулы

Таким образом, мы получили формулы (14.5)— (.14.8) языка логики предикатов первого порядка, аксиоматизирующие поведение оператора сети распределения и подачи воды при регулировании давления в контрольных точках. Две первые формулы включают кванторы. Вследствие конечного и сравнительно небольшого числа контрольных точек эти формулы легко преобразуются в эквивалентные, не содержащие кванторов формулы. Сначала избавимся от квантора существования. В результате получим формулы

(см. скан)

(см. скан)

Каждая из формул (14.11), (14.12) является формулой, состоящей из дизъюнкции импликаций, левая часть которых является конъюнкцией атомов, а правая состоит из одного атома. Очевидно, что для доказательства истинности такой формулы достаточно доказать истинность хотя бы одной импликации. Для доказательства же может быть использовано обобщенное правило модус поненс.

Аналогично можно получить формулы и по остальным схемам ситуаций. Выпишем их без комментариев.

14.3.3. Формулы регулирования скорости насосов

Получение формул регулирования скорости насосов легко проследить по рис. 14.7. Имеем

(см. скан)

14.3.4. Формулы регулирования уровня воды в резервуарах

Получение формул регулирования уровня воды в резервуарах легко проследить по рис. 14.8: