First-order logic Prolog anonymous variables

The following Prolog rule:

grandparent(X,Z) :- parent(X,Y) , parent(Y,Z)

      

First-order logic would:

∀x ∀y ∀z ((P (x, y) ∧ P (y, z)) → G(x, z))

      

In theory, if we have an anonymous variable in our Prolog rule something like this:

grandparent(X,Z) :- parent(X,Y, _ ) , parent(Y,Z, _ )

      

Let's say it's a surname, how can we represent it in first order logic?

+3


source to share


1 answer


Just use the rule:

"Give your child a name"

Note that the underscore is not a single variable. The two underscores in Prolog have nothing to do with each other.

We can just replace the code:



grandparent(X,Z) :-
    parent(X,Y,A),
    parent(Y,Z,B).
      

And now the logical "equivalent" would be:

∀x ∀y ∀z ∀a ∀b: ((P (x, y, a) ∧ P (y, z, b)) → G (x, z))

Note that these two characters are not equivalent : since in theory (perhaps not here) the first call parent/3

could have side effects, additional terms, etc. Only a subset of Prolog maps to such booleans.

+3


source







All Articles