Truth Assignments in Prolog

gistfile1.pl

% Truth Assignments for Classical Propositional Logica
% Adolfo Neto @adolfont https://github.com/adolfont
% August 24th, 2011

:- dynamic v/1.

% Definitions:
%  P is the set of propositional atoms
%  Example: P = {p1, p2, p3, ... }

% v is a truth assignment (valuation)
%  v: L(P) -> {t,f}
% where L(P) is the language of classical propositional logic
% and {t,f} is the set of truth-values

% Ane example of a valuation
v([p1,t]):-!.  % means v(p1)=t. In Prolog: v( [FORMULA, TRUTH-VALUE) ).
v([p2,t]):-!.
v([p3,f]):-!.

% ~p is represented as [not, p]
v([[not,X],t]):-v([X,f]),!.
v([[not,X],f]):-v([X,t]),!.

% (p&q) is represented as [p,and,q]
v([[X,and,Y],t]):-v([X,t]),v([Y,t]),!.
v([[_,and,_],f]):-!.

% (p|q) is represented as [p,or,q]
v([[X,or,Y],f]):-v([X,f]),v([Y,f]),!.
v([[_,or,_],t]):-!.

% (p->q) is represented as [p,implies,q]
v([[X,implies,Y],f]):-v([X,t]),v([Y,f]),!.
v([[_,implies,_],t]):-!.

/*

%% Tests run using SWI-Prolog (Multi-threaded, 32 bits, Version 5.10.1)

?- consult(truth_assignments).
% truth_assignments compiled 0.00 sec, 172 bytes
true.

?- v([p1,X]).
X = t.

?- v([p2,X]).
X = t.

?- v([[not,p1],X]).
X = f.

?- v([[not,p3],X]).
X = t.


?- v([[p1,or,p3],X]).
X = t.

?- v([[p3,or,p3],X]).
X = f.

?- v([[p3,implies,p3],X]).
X = t.

?- v([[p3,implies,p1],X]).
X = t.

?- v([[p1,implies,p3],X]).
X = f.
*/