====== Logic operators ======
{{tag>operators logic}}
===== Description =====
Satisfiability of Boolean formule

**Source**:  The Art of Prolog
===== Download =====
Program source code: {{logic_operators.pl}}
===== Listing =====
<code prolog>
/*
	satisfiable(Formula) :- 
		There is a true instance of the Boolean formula Formula.	     
*/
	:- op(950, xfx, [&]).
	:- op(950, xfx, [|]).
	:- op(900,  fx, [~]).


	satisfiable(true).
	satisfiable(X & Y) :- satisfiable(X), satisfiable(Y).
	satisfiable(X | Y) :- satisfiable(X).
	satisfiable(X | Y) :- satisfiable(Y).
	satisfiable((~ X)) :-  invalid(Y).
/*
	invalid(Formula) :-	
		There is a false instance of the Boolean formula Formula.	  
*/
	invalid(false).
	invalid(X | Y) :- invalid(X), invalid(Y).
	invalid(X & Y) :- invalid(X).
	invalid(X & Y) :- invalid(Y).
	invalid((~ X)) :- satisfiable(X).

%	Program 3.32: Satisfiability of Boolean formule
</code>
===== Comments =====