https://github.com/theoremprover-museum/CLIN
Raw File
Tip revision: e7082fbde3634286f458d64846699ae488fe18f3 authored by Michael Kohlhase on 22 December 2016, 09:28:55 UTC
initial commit, thanks to David Plaisted
Tip revision: e7082fb
clausify
%%% CLAUSIFY
%%%
%%% sprfn_to_clause:
%%% Transform a clause form in implication form to a general form.
%%%	head and body are separated by :- or equivalent operators.
%%%

%%% Declare the precedence of operators.
     :- op( 1200, xfx, [ : ]).
     :- op( 1200, xfx, [ :-- ]).
     :- op( 1200, xfx, [ :-. ]).

%%% Transform one clause each time.
%%% Head and body are separated by :-.
     sprfn_to_clause((X :- Y),C) :-
	make_and_list(Y, L1),
	make_or_list(X, L2),
	append(L2,L1,C), !.
%%% Head and body are separated by :--.
     sprfn_to_clause((X :-- Y),C) :-
	make_and_list(Y, L1),
	make_or_list(X, L2),
	append(L2,L1,C), !.
%%% Head and body are separated by :-..
     sprfn_to_clause((X :-. Y),C) :-
	make_and_list(Y, L1),
	make_or_list(X, L2),
	append(L2,L1,C), !.
%%% positive clause.
     sprfn_to_clause(X,C) :-
	make_or_list(X, C).

%%% Transform the body into a list.
     make_and_list((X,Y),Z) :-
	make_and_list(X,Z1),
	make_and_list(Y,Z2),
	append(Z1,Z2,Z), !.
     make_and_list(true,[]) :- !.
     make_and_list(X,[Y]) :- negate(X,Y).

%%% Transform the head into a list.
     make_or_list((X,Y),Z) :-
	make_or_list(X,Z1),
	make_or_list(Y,Z2),
	append(Z1,Z2,Z), !.
     make_or_list(false,[]) :- !.
     make_or_list(X,[X]).
back to top