如何在C中编写一阶逻辑公式？

Question

我是C的新手,也是stackoveflow的新手.我在编写第一个oder公式时遇到了一些问题

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

这里x是一个变量,暗示是谓词,f是函数.听起来对于所有x,x意味着x i的函数f(x).

使用C.任何建议和帮助将不胜感激.

Answer 1

一阶公式有布尔命题部分(在你的例子中,"implies(x,f(x))")和量词("Forall x").

您应该已经知道编写函数调用"f(x)"的编码在C语言中完全相同.

您使用逻辑连接符将命题部分编码为布尔C代码.对于您的示例,"implication"不是本机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 ...
}

如果任何命题实例为false,则"forall"为false,当您找到错误示例时,需要退出枚举:

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...

如果任何命题实例为true,则"exists"为true,因此当您找到真实结果时需要退出枚举:

// 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)) ...
    }
 }