如何用C语言编写一阶逻辑公式？

Question

我是 C 新手，也是 stackoveflow 新手。我在编码一阶公式时遇到一些问题，例如

forall([X],implies(X,f(X)))

这里 x 是变量，暗示是谓词，f 是函数。听起来对于所有 x，x 都意味着 x 的函数 i'e f(x)。

使用C。任何形式的建议和帮助将不胜感激。

Answer 1

一阶公式具有布尔命题部分（在您的示例中，“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 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)) ...
    }
 }

Answer 2

C 是一种命令式编程语言。这里的“命令”意味着执行是通过程序员明确告诉计算机要做什么来进行的。

对于你想要的， Prolog 更合适。它基于一阶谓词逻辑，并且通过尝试“找到由用户目标指定的否定查询的解析反驳”来执行。这种方法与 C 非常不同，因为执行更加隐式，并且意图的表达看起来也有很大不同。

如果您有大量时间，您可以用 C 编写自己的约束求解器或 Prolog 解释器，但默认情况下，C 对您正在寻找的内容没有一流的支持。