How to code first order logic formula in C?

Question

Hello, I am newbie in C and new to stackoveflow too. I have some problems in coding first oder formula like

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

Here x is a variable, implies is predicate and f is function. It sounds like for all x, x implies function of x i'e f(x).

using C. Any kind of suggestions and help will be appreciated.

Answer 1

C is an imperative programming language. "Imperative" here means that execution happens via the programmer specifically telling the computer what to do.

For what you want, Prolog is more appropriate. It is based on first-order predicate logic, and execution happens by trying to "find a resolution refutation of the negated query" that's specified by the user's goal. This approach is very unlike C since execution is much more implicit and the expression of intent looks much different.

If you have lots of time, you can write your own constraint solver or Prolog interpreter in C, but by default, C has no first-class support for what you're looking for.

Answer 2

First order formulas have boolean propositional parts (in your example, "implies(x,f(x))") and quantifiers ("Forall x").

You should already know that coding a function call "f(x)" is coded exactly that way in C.

You code the propositional part as boolean C code using logic connectives. For your example, "implication" isn't a native C operator so you have to substitute slightly different code for it. In c, the "?" operator does the trick. "a?b:c" produces "b" if "a" is true, and "c" otherwise. For your example:

   x?f(x):false

Quantifiers mean you have to enumerate the set of possible values of the quantified variable, which always has some abstract type. In logic, this set might be infinite, but it computers it is not. In your case, you need to enumerate the set of values which could be "x"s. To do that, you need a way to represent a set; a cheesy way to do that in C is to use an array to hold the set members X, and to iterate through the array:

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

Since a "forall" is false if any propositional instance is false, you need to exit the enumeration when you find a false example:

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" is true if any propositional instance is true, so you need to exit the enumeration when you find a true result:

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

If you have multiple quantifiers, you'll end up with nested loops, one loop for each quantifier. If your formula is complex, you'll likely need several intermediate boolean variables to compute the values of the various parts.

You'll also end up with a variety of "sets" (some arrays, some linked lists, some hash tables) so you'll need to learn how to use these data structures. Also, your quantified values might not be booleans, but that's OK; you can still pass them to functions that compute boolean values. To compute the FOL for:

 forall p:Person old(p) and forall f:Food ~likes(p,f)

the following code skeleton would be used (details left to the reader):

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