CODEWITHSUNDEEP
logicmaple
Robai
Robai

Reputation: 307

How to verify solutions for Logic functions having ampersand symbol (used in Logic package)

For example, if we have a logic function F = (x1 or x2) and (not x2) then we can verify a solution [x1=true, x2=false] of equation F = true this way:

[> F:=(x1 or x2) and (not x2):
   subs({x1=true,x2=false},F);
                                     true

Maple Logic package has a nice function Satisfy, which can find a solution, but function F (now it's named as G) has to be written using symbol & (before and, or, not):

[> G:=(x1 &or x2) &and (&not x2):
   A:=Logic[Satisfy](G);
                           A := {x1 = true, x2 = false}

But I don't know an easy way how to verify a solution (I mean not in this specific case, but in general, functions may have hundreds of variables). My attempt was to use substitution and then use evalb, but it didn't work:

[> G1:=subs(A,G);
   evalb(G1);
                   G1:= (true &or false) &and &not(false)
                      (true &or false) &and &not(false)

But for function F the substitution worked (even without evalb):

[> F1:=subs(A,F);
                                F1:=true

Also I couldn't find an easy way to remove ampersand symbol & from an expression (in order to construct function F from function G).

Upvotes: 2

Views: 78

Answers (2)

AmirHosein Sadeghimanesh
AmirHosein Sadeghimanesh

Reputation: 478

Another solution similar to @acer's, but the opposite direction. If you are not using anything else other than Satisfy from the Logic package and you are fine with having your logical formulas as in F in your example, then there is no need to have your formula saved in the Logic's style with ampersand operations. Instead of Export in @acer's answer, use Import. Here is how it works in your example.

F := (x1 or x2) and (not x2):
A := Logic:-Satisfy( Logic:-Import( F ) );
F1 := subs( A, F );

Note that Package:-Command is the same as Packae[Command] with tiny differences. You can also use eval( F, A ) instead of subs( A, F ). For their differences you can check Maple help pages. But here they give the same results as you want.

Upvotes: 1

acer
acer

Reputation: 7271

G := (x1 &or x2) &and (&not x2):

cand := {x1=true, x2=false}:

Given the logical expression assigned to G in form of used by the Logic package (ie. operators with names prefixed by &), then the candidate solution assigned to cand can be tested as follows:

BG := Logic:-Export(G, form=boolean);

      BG := (x1 or x2) and not x2

eval(BG, cand);

               true

Combining those two steps,

eval(Logic:-Export(G, form=boolean), cand);

               true

Upvotes: 2

Related Questions