Derivation and Proof Trees

Posted on | Post modified | In

Refutation in Predicate Logic

1
2
3
4
5
6
parent(pam, bob).
parent(tom, bob).
parent(tom, liz).
...
anc(X, Y):- parent(X, Y).
anc(X, Y):- parent(X, Z), anc(Z, Y).

  • Goal G:

    For what values of Q is :- anc(tom, Q) a logical consequence of the above program?

  • Negate the goal G:

    i.e. $\neg G \equiv \forall Q \neg anc(tom, Q).$

  • Consider the clauses in the program $P \cup \neg G$ and apply refutation

    • Note that a program clause written as

      $p(A, B):- q(A, C), r(B, C)$ can be rewritten as

      $\forall A, B, C (p(A, B) \or \neg q(A, C) \or \neg r(B, C))$

    i.e., l.h.s. literal is positive, while all r.h.s. literal are negative

    • Note also that all variables are universally quantified in a clause.

Refutation Examples

Unification

  • Operation done to ‘match’ the goal atom with the head of a clause in the program.
  • Forms the basis for the matching operation we used for Prolog evaluation:
    • f(a, Y) and f(X, b) unify when X=a and Y=b
    • f(a, X) and f(X, b) do not unify
      • f(a, X) = f(X, b) fails in Prolog

Substitutions

  • A substitution is a mapping between variables and values (terms)
    • Denoted by ${x_1/t_1, x_2/t_2, …,x_n/t_n}$ such that
      • $x_i \not= t_i$ ,and
      • $X_i$ and $X_j$ are distinct variables when $i \not = j$
    • The empty substitution is denoted by {} (or $\epsilon$).
    • …

Substitutions and Terms

Compusition of Substitutions

Idempotence

  • A substitution $\theta$ is idempotent iff

Unifiers

  • A substitution $\theta$ is a unifier of two terms s and t if $s\theta$ is identical to $t\theta$

    $\theta$ is a unifier of a set of equations ${s_1=t_1, …, s_n=t_n}$, if for all $i, s_i\theta=t_i\theta$

Equations and Unifiers

  • A set of equations E is in solved form if it is of the form

    ${x_1=t_1,…, x_n=t_n}$ Iff no $x_i$ appears in any $t_j$.

    • Given a set of equations $E={x_1=t_1,…, x_n=t_n}$, the substitution ${x_1/t_1, …, x_n/t_n}$ is an idempotent mug of $E$
    • Two sets of equations $E_1$ and $E_2$ are said to be equivalent iff they have the same set of unifiers.
    • To find the mgu of two terms s and t, try to find a set of equations in solved form that is equivalent to $$