PLOGHELP CLAUSIFY                        Kathryn Seifert  September 1986

Library program for changing predicate calculus formulae to clausal form

Keywords: normal form, clausal form, logic, theorem proving,
          predicate calculus


-- INTRODUCTION -------------------------------------------------------

LIB * CLAUSIFY is a program which translates propositions in the
predicate calculus to clausal form (see PLOGHELP * RESOLVE, TEACH *
RESOLUTION).  This library file is to be used in conjunction with
LIB * RESOLVE1  and LIB * RESOLVE2 (see PLOGHELP * RESOLVE and
TEACH * RESOLUTION).

-- NOTATION -----------------------------------------------------------

The predicate calculus formulae to be translated should use the
following notation:

 LOGICAL OPERATION          PROLOG OPERATOR
 -----------------          ---------------

    NOT                 :       #
    OR                  :       v
    AND                 :       ^
    IMPLIES             :       ->
    EQUIVALENT          :       <->

Logical variables in the predicate calculus formulae should be
represented by Prolog variables.  Quantification over variables should
be represented in the following way:

    Universal quantification:   all(X, P).
    (Where X is a variable and P is a proposition)

    Existential quantification: exists(X, P).
    (Where X is a variable and P is a proposition)

-- EXAMPLES -----------------------------------------------------------

Here are some examples of LIB * CLAUSIFY at work:

    ?- library(clausify).
    yes


Finding the clausal form of "All men are mortal":

    ?- clausify(all(X, man(X) -> mortal(X)), Y).
    X = _1
    Y = [fact [# man(_1), mortal(_1)]] ?
    yes

Finding the clausal form of "All mothers have a child":

    ?- clausify(all(X, exists(Y, mother(X) -> child(Y, X))), Z).
    X = _3
    Y = f1(_3)
    Z = [fact [# mother(_3), child(f1(_3), _3)]] ?
    yes

-- RELATED DOCUMENTATION ----------------------------------------------

PLOGHELP * RESOLVE
 Teaching packages for resolution theorem proving

TEACH * RESOLUTION
 Tutorial introduction to resolution and relation of logic to Prolog