Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
:- op(100, fy, ?). :- op(200, fy, ~). :- op(500, yfx, and). :- op(500, yfx, or). :- op(690, yfx, =>). :- op(700, yfx, <=>). table(F, T) :- term_variables(F, Vs), bagof(R-Vs, bl(F, R), T). valid(F) :- forall(bl(F, R), R == t). contradiction(F) :- forall(bl(F, R), R == f). lequiv(F, G) :- forall(( bl(F, X), bl(G, Y) ), X == Y). bl(?X, R) :- v(X, R). bl(~X, R) :- bl(X, R0), not(R0, R). bl(X and Y, R) :- bl(X, R0), and_bl(R0, Y, R). bl(X or Y, R) :- bl(X, R0), or_bl(R0, Y, R). bl(X => Y, R) :- bl(X, R0), impl_bl(R0, Y, R). bl(X <=> Y, R) :- bl(X, R0), bl(Y, R1), eq(R0, R1, R). bl(X xor Y, R) :- bl(X, R0), bl(Y, R1), xor(R0, R1, R). v(f, f). v(t, t). not(t, f). not(f, t). and_bl(f, _, f). and_bl(t, Y, R) :- bl(Y, R). or_bl(f, Y, R) :- bl(Y, R). or_bl(t, _, t). impl_bl(t, Y, R) :- bl(Y, R). impl_bl(f, _, t). eq(f, Y, R) :- not(Y, R). eq(t, Y, Y). xor(f, Y, Y). xor(t, Y, R) :- not(Y, R).