Без заголовка

Хорошо. Предлагаю завершить дискуссию на следующем тезисе. Дескрипционная логика http://ru.wikipedia.org/wiki/Дескрипционная_логика, которая предоставляет богатый аппарат для накопления и верификации знаний (частный случай - знания о соответствии системы требованиям), а также дает инструментарий для вывода, конечно сводима к предикатам. Однако структурная информация (об архитектуре и процессах в системе) в ней может быть отделена от информации предметной (как конкретно действует тот или иной элемент). В силу того, что многие системы (особено антропоцентрические) предполагают по умолчанию возможность изменения требований, то доказать правильность системы можно только в каком-то одном view point. Например, с точки зрения текущего реестра требований. Или с точки зрения эффективности процедур адаптации системы к новым требвоаниям. Для первого предикативная форма возможна, но вероятно, не очень удобна, особенно в контексте вычислимости (всякое ли требование или суперпозицию требований можно представить в виде вычислимого предиката, а также даже зная конкретный вид предиката - для каждого ли можно алгоритмически найти процедуру, которая обернет этот предикат в единицу). Для второго - переходить от структурного описания в дескрипционной логике к ее предикативному отоборажению бессмысленно, т.к. именно структурная (процессная) информация является определяющей, и соответственно, доказательство правильнее всего строить в дескрипционной логике. Если не согласны - любопытно, в чем.