Наша цель формализовать en-высказывания которые предложил JFS. Для этого мы сопоставим им логически эквивалентные ru-высказывания, которые и будут формализованы. Логическая эквивалентность высказываний рассматривается в рамках простой математической модели строения молекулы - помеченный граф.
Не вдаваясь в сложившуюся систему наук будем считать для простоты что мы в физике строения молекул. (см. [ЛЛ-3] с.464 глава XIII "Многоатомные молекулы"). Принципиальная задача - рассчитать устойчивую конфигурацию (пространственное расположение) совокупности из N неподвижных ядер, окружённых n электронами.
Уже соединяя ближайшие ядра такой конфигурации воображаемыми отрезками мы получим геометрическую фигуру - "многорёберник", а отвлекаясь от расстояний и углов - норграф.
Не вдаваясь в тонкости понятия химической связи (ведь непосредственно мы имеем распределение электронов вокруг ядер) будем считать что видов хим-связи в молекуле бензола всего два: HC-связь - водород-углерод и СCb-связь - углерод-углерод где добавка b подчёркивает что это бензольная связь когда 3(?) электрона участвуют во всех шести ССb-связях.
Итак, для строения молекулы есть такие математические абстракции:
- геометрическая точечная(!) фигура расположения ядер в двумерном(как оказалось!) пространстве: углерода - в вершинах правильного 6-ти угольника со стороной 139пм и водорода на внешних лучах от центра на расстоянии 109пм от ядер углерода [см. рис.] (ясно что ядра водорода тоже в вершинах 6-и угольника),
- многорёберник связей,
- норграф связей между ядрами (см. на отрезки на предыдущем рисунке как на дуги).
Высказывания предложенные JFS для формализации относятся к норграфу. Тем самым с точки зрения соревнования языков следует отметить, что трудности формализации (если есть) это трудности математические, а именно формализации теории графов /ТГ/, возможно даже чистой ТГ, т.е. без меток. То есть не имеют прямого отношения к онтологистике;-)
Норграф строения молекулы это норгаф в котором узлы помечены идентификатором химического элемента, а дуги - идентификатором вида химической связи.
Свойства НСМ предложенные для формализации JFS расположены в таблице ТС1 (см. далее) в колонке CEL, в колонке КРЯ имеем их перевод, а в колонке 3 - формализацию в основном на YAFOLL или где-то рядом (Y!L+).
Декомпозиция сложных предложений на простые - по ходу дела перевода.
Y!L формализация опирается на сигнатуру норгафа <V, E; inc(V E):TV> [см.] к которой добавляются функции: l - метка узла, имеющая сигнатуру V:String; и le метка дуги, имеющая сигнатуру E:String.
Под-граф будем задавать контуром его дуг [см.].
Обозначения:
# - квантор количества: количество элементов области пробега удовлетворяющих предикату.
∃! - существует единственный.
Def - унарный супер-оператор, принимающий на вход любую функцию и возвращающий предикат той же сигнатуры аргументов. Предикат истинный тогда и только тогда, когда функция имеет значение на данных аргументах. Def полезен для частичных функций - задаёт их область определённости.
Предикат Contour определен в [см.] а ring в [???].
+У: из "Кольцо есть простой цикл но не петля." сразу следует что Contour из формализации можно удалить;-)
Замечания к 3).
б) Переформулировка 321 подчёркивает факт существования под-графа - кольца и указывает его через свойство его дуг. В большинстве случаев под-граф можно указать именно составом его дуг, а не вершин.
в) То что атомы углерода соединены в кольцо CCb-связями, является очевидным следствием из ring(r), и это высказывание предлагается не формализовывать из принципа: формализовывать надо не всё, а скорее всего минимум;-) В данном случае речь идёт о том, что 3) первоначально могло быть сформулировано как "Все CCb-связи образуют кольцо при этом каждый атом углерода связан ровно с двумя другими атомами углерода".
Замечание к 4). Мы не рассматриваем высказывание 4) как индуктивное определение отношения "is connected" так как обычно в теории графов определение связности даётся через существование пути. В первом приближении высказывание 4) есть переформулировка в терминах предметной области теоремы теории графов "Узел X связан с узлом Y тогда и только тогда когда X соединён с Y или X соединён с узлом Z который связан с Y.";-) Переход к индуктивному определению в теории графов здесь рассматривать не след.
Очевидно что можно написать такую совокупность свойств помеченного норграфа, что они опишут его с точностью до изоморфизма. Свойств колонки 2, а значит и 1, для этого не достаточно.
Чтобы задать мат-модель (помеченный норграф) нам надо:
Во-первых нам надо задать норграф молекулы бензола, что делается систематическим образом как и для любого графа: перечисляется состав узлов, дуг и отношение инцидентности между ними. На ЕЯ это делается регулярным образом:
В норгафе молекулы бензола 12 узлов, обозначим их у1,... у6 и в1,... в6.
В норгафе молекулы бензола 12 рёбер, обозначим их ву1,... ву6 и ууб1,... ууб6.
ву1 инцидентны в1 и у1,... ву6 инцидентны в6 и у6.
ууб1 инцидентны у1 и у2,... ууб5 инцидентны у5 и у6.
ууб6 инцидентны у6 и у1.
Во-вторых нам надо его пометить:
Метки у1,... у6 - "C". Метки в1,... в6 - "H". Метки ву1,... ву6 - "HC". Метки уу1,... уу6 - "CCb".
Обозначим этот граф НГБ. Если у нас есть средство ("процессор") в котором можно задавать помеченные графы, а за тем вычислить на них формулы, в том числе колонки 3 ТС1, то мы сможем проверить что НГБ им удовлетворяет. То есть, переходя к терминологии предметной области: молекула бензола удовлетворяет свойствам колонки 2.
На конечной модели формулы первого порядка вычисляются по меньшей мере перебором и мы вправе ожидать что процессор языка Y!L умеет их вычислять.
Формулы "высокого порядка" (HOL) (а у нас такова 331) конечно тоже можно вычислить перебором. В данном случае мы имеем фразу ∃r:(E:E) и на заданном норграфе надо перебрать все функциональные подмножества ExE, т.е. все частичные унарные функции из E в E. Ясно что их конечное число.
Но проще поручить эту задачу специальному процессору - машина вывода графов /МВГ/. Этот процессор получает на вход норгаф и выдаёт на выходе 0 или более контуров держащих все кольца данного графа.
Мы работали с очень простой математической моделью молекулы. Конечно уже она полезна и важна, так к ней можно обращаться (задавать вопросы) не обращаясь непосредственно к молекуле (бензола в нашем случае). Например, если кого-то заинтересует расстояние между противоположными ядрами углерода, то их можно вычислить геометрически. И здесь можно поднять вопрос о машине вывода планарной (для бензола) геометрии и алгоритме А. Тарского.
Конечно на практике и в общем случае новый запрос потребует исследовательской работы, которая обычно завершается формулой или алгоритмом задания функции ответа. Так для примера выше формула - 2*r, где r - расстояние между ближайшими ядрами углерода и ответ будет 278пм. Конечно в саму мат-модель надо добавить длину дуг графа, что и перенесёт нас в геометрию. Ну а для полноты - углы, либо, регулярным образом: координаты конфигурации ядер в некоторой декартовой системе координат.
Трудности формализации конечно не относятся к науке предметной области (физике молекул) - они в формализации некоторых положений ТГ - формализации понятия кольца. Причём в классической ТГ предикат связности определяется через существование пути, т.е. "стихийно" (по сути дела) находится за пределами FOL:-)
Литература
[ЛЛ-3] Ландавшиц, т.3