Translating a propositional calculus formula into a set of (asserted) clauses.

Source: PROLOG programming for artificial intelligence, 3rd Edition, Harlow, 2001, ISBN 0-201-40375-7.

Program source code: propositional_calculus_2_clauses.pl

%  Figure 23.16  Translating a propositional calculus formula into
%  a set of (asserted) clauses.
 
 
%  Translating a propositional formula into (asserted) clauses
 
:-  op( 100, fy, ~).        % Negation
:-  op( 110, xfy, &).       % Conjunction
:-  op( 120, xfy, v).       % Disjunction
:-  op( 130, xfy, =>).      % Implication
 
% translate( Formula): translate propositional Formula
%   into clauses and assert each resulting clause C as clause( C)
 
translate( F & G)  :-                    % Translate conjunctive formula
  !,                                     % Red cut
  translate( F),
  translate( G).
 
translate( Formula)  :-
  transform( Formula, NewFormula),       % Transformation step on Formula
  !,                                     % Red cut
  translate( NewFormula).
 
translate( Formula)  :-                  % No more transformation possible
  assert( clause( Formula)).
 
% Transformation rules for propositional formulas
 
% transform( Formula1, Formula2)  if
%   Formula2 is equivalent to Formula1, but closer to clause form
 
transform( ~(~X), X).                      % Eliminate double negation
 
transform( X => Y, ~X v Y).                % Eliminate implication
 
transform( ~ (X & Y), ~X v ~Y).            % De Morgan's law
 
transform( ~ (X v Y), ~X & ~Y).            % De Morgan's law
 
transform( X & Y v Z, (X v Z) & (Y v Z)).  % Distribution
 
transform( X v Y & Z, (X v Y) & (X v Z)).  % Distribution
 
transform( X v Y, X1 v Y)  :-
  transform( X, X1).                       % Transform subexpression
 
transform( X v Y, X v Y1)  :-
  transform( Y, Y1).                       % Transform subexpression
 
transform( ~ X, ~ X1)  :-              
  transform( X, X1).                       % Transform subexpression