% FULL PROPOSITIONAL LOGIC % % Intuitive readings for predicates: % % true(F) = Formula F is true % sat(F) = Formula F must be satisfied % % Function symbols for propositional connectives: % % a(F1,F2) for the "and" of F1 and F2 % o(F1,F2) for the "or" of F1 and F2 % n(F) for the "not" of F %%% DOMAIN RULES %%% % Determine the subformulas (compound and atomic) of the given formulas sub(S) :- sat(S). sub(S1;S2) :- sub(a(S1,S2)). sub(S1;S2) :- sub(o(S1,S2)). sub(S1;S2) :- sub(i(S1,S2)). sub(S) :- sub(n(S)). comp(a(S1,S2)) :- sub(a(S1,S2)). comp(o(S1,S2)) :- sub(o(S1,S2)). comp(i(S1,S2)) :- sub(i(S1,S2)). comp(n(S)) :- sub(n(S)). atom(S) :- sub(S), not comp(S). %%% CLAUSES DEFINING SOLUTIONS %%% % Tseitin transformation true(a(S1,S2)) | -true(S1) | -true(S2) :- comp(a(S1,S2)). -true(a(S1,S2)) | true(S1) :- comp(a(S1,S2)). -true(a(S1,S2)) | true(S2) :- comp(a(S1,S2)). true(o(S1,S2)) | -true(S1) :- comp(o(S1,S2)). true(o(S1,S2)) | -true(S2) :- comp(o(S1,S2)). -true(o(S1,S2)) | true(S1) | true(S2) :- comp(o(S1,S2)). true(i(S1,S2)) | true(S1) :- comp(i(S1,S2)). true(i(S1,S2)) | -true(S2) :- comp(i(S1,S2)). -true(i(S1,S2)) | -true(S1) | true(S2) :- comp(i(S1,S2)). true(n(S)) | true(S) :- comp(n(S)). -true(n(S)) | -true(S) :- comp(n(S)). % Enforce satisfaction true(S) :- sat(S). % Couple of trivial instances for testing purposes % sat(a(p,n(p))). % No models % sat(o(p,n(p))). % Tautology %%% PROJECT SOLUTIONS %%% #hide. #show true(S): atom(S). #show -true(S): atom(S).