<div class="notebook"> <div class="nb-cell html" name="htm1"> Valuation of propositional formula.<br> With dynamic table. </div> <div class="nb-cell program" data-singleline="true" name="p1"> /* * Warranty * Liability * To the extent permitted by applicable law and unless explicitly * otherwise agreed upon, XLOG Technologies GmbH makes no warranties * regarding the provided information. XLOG Technologies GmbH assumes * no liability that any problems might be solved with the information * provided by XLOG Technologies GmbH. * * Rights * License * All industrial property rights regarding the information - copyright * and patent rights in particular - are the sole property of XLOG * Technologies GmbH. If the company was not the originator of some * excerpts, XLOG Technologies GmbH has at least obtained the right to * reproduce, change and translate the information. * * Reproduction is restricted to the whole unaltered document. Reproduction * of the information is only allowed for non-commercial uses. Selling, * giving away or letting of the execution of the library is prohibited. * The library can be distributed as part of your applications and libraries * for execution provided this comment remains unchanged. * * Restrictions * Only to be distributed with programs that add significant and primary * functionality to the library. Not to be distributed with additional * software intended to replace any components of the library. * * Trademarks * Jekejeke is a registered trademark of XLOG Technologies GmbH. */ :- use_rendering(table). :- op(300, fy, ~). /* * eval(A, R): * The predicate succeeds in R with a partial evaluated * Boolean formula. The predicate starts with the leaves * and calls simp after forming new nodes. */ % eval(+Formula, -Formula) eval(A=<B, R) :- !, eval(A, X), eval(B, Y), simp(X=<Y, R). eval(A=:=B, R) :- !, eval(A, X), eval(B, Y), simp(X=:=Y, R). eval(A+B, R) :- !, eval(A, X), eval(B, Y), simp(X+Y, R). eval(A*B, R) :- !, eval(A, X), eval(B, Y), simp(X*Y, R). eval(~A, R) :- !, eval(A, X), simp(~X, R). eval(A, A). /* * atoms(A, L): * The predicate succeeds in L with the propositonal * variables of the formula A. The predicate starts with * the leaves and unions in the nodes. */ % atoms(+Formula, -List) atoms(A=<B, R) :- !, atoms(A, X), atoms(B, Y), union(X, Y, R). atoms(A=:=B, R) :- !, atoms(A, X), atoms(B, Y), union(X, Y, R). atoms(A+B, R) :- !, atoms(A, X), atoms(B, Y), union(X, Y, R). atoms(A*B, R) :- !, atoms(A, X), atoms(B, Y), union(X, Y, R). atoms(~A, X) :- !, atoms(A, X). atoms(A, X) :- atom(A), !, X = [A]. atoms(_, []). /* * subst(A, X, T, B): * The predicate succeeds in B with the substitution A[X/T]. * The predicate starts with the leaves and checks whether a * leave equals the given propositional variable X or not. * If it equals the leave is replaced by the formula T. */ % subst(+Formula, +Variable, +Formula, -Formula) subst(A=<B, X, T, U=<V) :- !, subst(A, X, T, U), subst(B, X, T, V). subst(A=:=B, X, T, U=:=V) :- !, subst(A, X, T, U), subst(B, X, T, V). subst(A+B, X, T, U+V) :- !, subst(A, X, T, U), subst(B, X, T, V). subst(A*B, X, T, U*V) :- !, subst(A, X, T, U), subst(B, X, T, V). subst(~A, X, T, ~U) :- !, subst(A, X, T, U). subst(A, X, T, U) :- A = X, !, U = T. subst(A, _, _, A). /* * simp(A, B): * The predicate succeeds in B with a simpler formula than A, * or if an immediately simpler formula is not possible with * formula B itself. */ % simp(+Formula, -Formula) simp(0=<_, 1) :- !. simp(A=<0, X) :- !, simp(~A, X). simp(1=<B, B) :- !. simp(_=<1, 1) :- !. simp(0=:=B, X) :- !, simp(~B, X). simp(A=:=0, X) :- !, simp(~A, X). simp(1=:=B, B) :- !. simp(A=:=1, A) :- !. simp(0+B, B) :- !. simp(A+0, A) :- !. simp(1+_, 1) :- !. simp(_+1, 1) :- !. simp(0*_, 0) :- !. simp(_*0, 0) :- !. simp(1*B, B) :- !. simp(A*1, A) :- !. simp(~0, 1) :- !. simp(~1, 0) :- !. simp(A, A). /* * valuation(F, L, R): * The predicate succeeds in L with all possible variable * association and in R with the corresponding valuation * of the formula F. */ % valuation(+Form, -Table) valuation(F, [J|R]) :- atoms(F, K), sort(K, H), append(H, [F], J), valuation(F, H, [], R, []). % valuation(+Form, +List, +List, -Table, +Table) valuation(F, [B|H], L, I, O) :- subst(F, B, 0, P), valuation(P, H, [0|L], I, J), subst(F, B, 1, Q), valuation(Q, H, [1|L], J, O). valuation(F, [], L, [J|R], R) :- eval(F, G), reverse(L, H), append(H, [G], J). </div> <div class="nb-cell html" name="htm6"> In propositional logic, an assignment of truth<br> values to propositional variables, with a corresponding<br> assignment of truth values to all propositional<br> formulas with those variables.<br> <a href="https://en.wikipedia.org/wiki/Valuation_%28logic%29">Wikipedia - Valuation (Logic)</a> </div> <div class="nb-cell html" name="htm2"> The tautology A∨¬A always valuates to ⊤. </div> <div class="nb-cell query" data-chunk="10" name="q1"> valuation(a+ ~a, L). </div> <div class="nb-cell html" name="htm3"> The formula A∨¬B does not always valuate to ⊤, so its not a tautology. </div> <div class="nb-cell query" data-chunk="10" name="q2"> valuation(a+ ~b, L). </div> <div class="nb-cell html" name="htm4"> Try it yourself: </div> <div class="nb-cell query" data-chunk="10" name="q3"> projection([L]), parameters([F:label('Formula')]), valuation(F,L). </div> <div class="nb-cell html" name="htm5"> More propositional logic Prolog notebooks here:<br> <a href="https://swish.swi-prolog.org/p/Logic.swinb">Logic</a> </div> </div>