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