Stephan Lukits schrieb:
> Hello,
> is there something like:
>
> (%i1) (am and (gg or gn)) equiv ((am and gg) or (am and gn));
> (%o1) true
Since no one answered and I couldn't find something like this
in the documentation, I wrote it my self. Kind a worm up in
programming maxima.
Maybe some one else thinks thats useful, thus I post the
implementation of a logical equivalence operator "=|="
and a logical implecation operator "|=".
Or maybe some one is so kind and would like to give me
a lesson improving my coding. (I already know that the
implementations share some code. But I decided against
splitting it into functions since I do not want to pollute
the name space)
infix ("=|=",40,40, clause, clause, clause);
"=|="(exp1, exp2)
/*Returns true if exp1 and exp2 are logicaly equivalent; otherwise
*false is returned and a variable assignement is displayed where the
*equivalence brakes. One shouldn't use 'exp1' or 'exp2' literally as
*variable names for the arguments of =|=. */
:= block(
/*makes a list which contains n-times item*/
makeNList(n, item) := block(
if n = 0 then return([])
else
returnVal:cons(item,[]),
for a:2 step 1 thru n do
returnVal:cons(item,returnVal),
return(returnVal)),
/*tests for constant expressions*/
if is(listofvars(exp1) = []) and is(listofvars(exp2) = []) then
/*evaluate constant expressions*/
return(is(exp1 = exp2)),
vars:if is(listofvars(exp1) = []) then
listofvars(exp2)
else
listofvars(exp1),
/*returns false if variables in exp1 and exp2 are not the same
*and non of both is a logical constant.
*/
if not(is(equal(listofvars(exp1), []))
or is(equal(listofvars(exp1), [])))
and not(is(setify(listofvars(exp1)) =
setify(listofvars(exp2)))) then
return(false),
/*generates {true,false}^n for the n variables of vars*/
trueFalsePermutations:block(
returnValue:{},
for i:0 step 1 thru length(vars) do
returnValue:union(permutations(
append(makeNList(i,false),
makeNList((length(vars)-i),true))),
returnValue),
return(returnValue)),
/*creates all possible variable assigenments. An alternative
*coding which generates and test assigenments one by one would
*be desireable*/
variableTrueFalseCases:
map(lambda([tf],map("=",vars,tf)),
listify(trueFalsePermutations)),
p:true, /*returned if exp1 and exp2 evaluate to the same
*truth value with identically variable assigenments*/
for tfc in variableTrueFalseCases while p do
/*tests if exp1 and exp2 evaluate to the same truth value
*having the same variable assigenments*/
if not(is(equal(at(exp1,tfc), at(exp2,tfc)))) then
/*evaluating not to the same truth value they are not
*logically equivalent*/
block( disp(tfc), p:false),
p);
infix ("|=",40,40,clause,clause,clause);
"|="(exp1, exp2)
/*Returns true if exp1 implies exp2 logicaly; otherwise false is
*returned and a variable assignement is displayed where the
*implication brakes. One shouldn't use 'exp1' or 'exp2' literally as
*variable names for the arguments of =|=. */
:= block(
/*makes a list which contains n-times item*/
makeNList(n, item) := block(
if n = 0 then return([])
else
returnVal:cons(item,[]),
for a:2 step 1 thru n do
returnVal:cons(item,returnVal),
return(returnVal)),
/*tests for constant expressions*/
if is(listofvars(exp1) = []) and is(listofvars(exp2) = []) then
/*evaluate constant expressions*/
if is(exp1 = true) and is(exp2 = false) then
return(false)
else
return(true),
vars:if is(length(listofvars(exp1)) < length(listofvars(exp2))) then
listofvars(exp2)
else
listofvars(exp1),
/*generates {true,false}^n for the n variables of vars*/
trueFalsePermutations:block(
returnValue:{},
for i:0 step 1 thru length(vars) do
returnValue:union(permutations(
append(makeNList(i,false),
makeNList((length(vars)-i),true))),
returnValue),
return(returnValue)),
/*creates all possible variable assigenments. An alternative
*coding which generates and test assigenments one by one would
*be desireable*/
variableTrueFalseCases:
map(lambda([tf],map("=",vars,tf)),
listify(trueFalsePermutations)),
p:true, /*returned if exp1 and exp2 evaluate to the same
*truth value with identically variable assigenments*/
for tfc in variableTrueFalseCases while p do
/*tests if exp1 evalueates to true if exp2 does
*having the same variable assigenments*/
if is(equal(at(exp1,tfc), true))
and is(equal(at(exp2,tfc), false)) then
/*exp2 evaluating to true whereas exp1 dosen, exp1
*doesn't logically imply exp2*/
block( disp(tfc), p:false),
p);
/***************TESTS********************************/
if not(true =|= false) then print("'true =|= false': OK")
else print("'true =|= false': FAIL");
if (true =|= true) then print("'true =|= true': OK")
else print("'true =|= true': FAIL");
if (false =|= false) then print("'false =|= false': OK")
else print("'false =|= false': FAIL");
if not(false =|= true) then print("'false =|= true': OK")
else print("'false =|= true': FAIL");
if (true and true =|= true) then print("'true and true =|= true': OK")
else print("'true and true =|= true': FAIL");
if not(true and false =|= true) then print("'true and false =|= true': OK")
else print("'true and false =|= true': FAIL");
if not(true =|= true and false) then print("'true =|= true and false': OK")
else print("'true =|= true and false': FAIL");
if not(true =|= false and false) then print("'true =|= false and false':
OK")
else print("'true =|= false and false': FAIL");
if (true or true =|= true) then print("'true or true =|= true': OK")
else print("'true or true =|= true': FAIL");
if (true or false =|= true) then print("'true or false =|= true': OK")
else print("'true or false =|= true': FAIL");
if not(a =|= true) then print("'a =|= true': OK")
else print("'a =|= true': FIAL");
if not(true =|= a) then print("'true =|= a': OK")
else print("'true =|= a': FAIL");
if (a =|= a) then print("'a =|= a': OK")
else print("'a =|= a': FAIL");
if (a or true =|= true) then print("'a or true =|= true': OK")
else print("'a or true =|= true': FAIL");
if not(a or true =|= false) then print("'a or true =|= false': OK")
else print("'a or true =|= false': FAIL");
if (true =|= a or true) then print("'true =|= a or true': OK")
else print("'true =|= a or true': FAIL");
if not(false =|= a or true) then print("'not(false =|= a or true)': OK")
else print("'not(false =|= a or true)': FAIL");
if (a and true =|= a) then print("'(a and true =|= a)': OK")
else print("'(a and true =|= a)': FAIL");
if (a =|= a and true) then print("'(a =|= a and true)': OK")
else print("'(a =|= a and true)': FAIL");
if (a and false =|= false) then print("'(a and false =|= false)': OK")
else print("'(a and false =|= false)': FAIL");
if not(a and false =|= true) then print("'(a and false =|= true)': OK")
else print("'(a and false =|= true)': FAIL");
if (a and b =|= b and a) then print("'(a and b =|= b and a)': OK")
else print("'(a and b =|= b and a)': FAIL");
if (a or b =|= b or a) then print("'(a or b =|= b or a)': OK")
else print("'(a or b =|= b or a)': FAIL");
if ((a and b) and c =|= a and (b and c)) then
print("'((a and b) and c =|= a and (b and c))': OK")
else print("'((a and b) and c =|= a and (b and c))': FAIL");
if ((a or b) or c =|= a or (b or c)) then
print("'((a or b) or c =|= a or (b or c))': OK")
else print("'((a or b) or c =|= a or (b or c))': FAIL");
if not(a and b =|= not(a) or not(b)) then
print("'a and b =|= not(a) or not(b)': OK")
else print("'a and b =|= not(a) or not(b)': FAIL");
if (not(a and b) =|= not(a) or not(b)) then
print("'not(a and b) =|= not(a) or not(b)': OK")
else print("'not(a and b) =|= not(a) or not(b)': FAIL");
if not(a and b =|= b) then print("'a and b =|= b': OK")
else print("'a and b =|= b': FAIL");
if (true |= true) then print("'true |= true': OK")
else print("'true |= true': FAIL");
if not(true |= false) then print("'true |= false': OK")
else print("'true |= false': FAIL");
if not(a |= false) then print("'a |= false': OK")
else print("'a |= false': FAIL");
if (a |= true) then print("'a |= true': OK")
else print("'a |= true': FAIL");
if not(true |= a) then print("'true |= a': OK")
else print("'true |= a': FAIL");
if (false |= a) then print("'false |= a': OK")
else print("'false |= a': FAIL");
if (a and b |= true) then print("'a and b |= true': OK")
else print("'a and b |= true': FAIL");
if (a and b |= a) then print("'a and b |= a': OK")
else print("'a and b |= a': FAIL");
if (a and b |= b) then print("'a and b |= b': OK")
else print("'a and b |= b': FAIL");
if (a |= a or b) then print("'a |= a or b': OK")
else print("'a |= a or b': FAIL");
if (b |= a or b) then print("'b |= a or b': OK")
else print("'b |= a or b': FAIL");
if not(not(a and b) or c |= (not(a) or c) and (not(b) or c)) then
print("'not(a and b) or c |= (not(a) or c) and (not(b) or c)': OK")
else print("'not(a and b) or c |= (not(a) or c) and (not(b) or c)':
FAIL");