Search code examples
logicmaple

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).


Solution

  • 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