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