一阶公式具有布尔命题部分（在您的示例中为“implies(x,f(x))”）和量词（“Forall x”）。
您应该已经知道在 C 中编写函数调用“f(x)”的编码方式正是如此。
您使用逻辑连接将命题部分编码为布尔 C 代码。对于您的示例，“暗示”不是本机 C 运算符，因此您必须为它替换稍有不同的代码。在 c 中，“？”运营商做到了。如果“a”为真，“a?b:c”产生“b”，否则产生“c”。以您为例：
x?f(x):false
量词意味着你必须枚举量化变量的一组可能值，它总是有一些抽象类型。在逻辑上，这个集合可能是无限的，但它不是。在您的情况下，您需要枚举可能是“x”的值集。为此，您需要一种表示集合的方法；在 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”为真，因此当找到真结果时需要退出枚举：
// 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)) ...
}
}