Формулы первого порядка имеют логические пропозициональные части (в вашем примере «подразумевает (x, f (x))») и квантификаторы («Forall x»).
Вы уже должны знать, что кодирование вызова функции "f (x)" точно так же кодируется в C.
Вы кодируете пропозициональную часть как логический C-код, используя логические связки. В вашем примере «implication» не является собственным оператором C, поэтому вам придется заменить его немного другим кодом. В с "?" Оператор делает свое дело. «a? b: c» производит «b», если «a» истинно, и «c» в противном случае. Для вашего примера:
x?f(x):false
Квантификаторы означают, что вам нужно перечислить набор возможных значений квантифицированной переменной, которая всегда имеет некоторый абстрактный тип. В логике этот набор может быть бесконечным, но это компьютеры, это не так. В вашем случае вам нужно перечислить набор значений, которые могут быть «х». Для этого вам нужен способ представления набора; Самый простой способ сделать это в C - использовать массив для хранения членов набора X и перебора массива:
type_of_x set_of_x[1000];
... fill x somehow ...
for(i=1;i<number_of_set_elements;i++)
{ x= set_of_x[i];
... evaluate formula ...
}
Поскольку «forall» является ложным, если любой пропозициональный экземпляр является ложным, вам нужно выйти из перечисления, когда вы найдете ложный пример:
boolean set_of_x[1000]; // in your example, x must be a boolean variable
// forall x
... fill x somehow ...
final_value=true;
for (i=1;i<number_set_elements; i++)
{ x= set_of_x[i];
if (x?f(x):false)
{ final_value=false;
break;
}
}
... final_value set correctly here...
«существует» - это истина, если любой пропозициональный экземпляр истинен, поэтому вам нужно выйти из перечисления, когда вы найдете верный результат:
// exists x
... fill x somehow ...
final_value=false;
for (i=1;i<number_set_elements; i++)
{ x= set_of_x[i];
if (x?f(x):false)
{ final_value=true;
break;
}
}
... final_value set correctly here...
Если у вас есть несколько квантификаторов, вы получите вложенные циклы, по одному циклу для каждого квантификатора. Если ваша формула сложная, вам, вероятно, понадобится несколько промежуточных логических переменных для вычисления значений различных частей.
Вы также получите множество «наборов» (несколько массивов, несколько связанных списков, несколько хеш-таблиц), поэтому вам необходимо научиться использовать эти структуры данных. Кроме того, ваши количественные значения могут быть не булевыми, но это нормально;
вы все равно можете передать их функциям, которые вычисляют логические значения. Для вычисления FOL для:
forall p:Person old(p) and forall f:Food ~likes(p,f)
будет использоваться следующий фрагмент кода (подробности предоставлены читателю):
person array_of_persons[...];
foods array_of_foods[...]
for (i=...
{ p=array_of_persons[i];
is_old = old(p);
for(j=...
{ f=array_of_foods[j];
...
if (is_old && !likes(p,f)) ...
}
}