¿Algún software libre para calcular expresiones booleanas?

Este procedimiento de Python evaluará una fórmula en su formato (primer argumento) contra una lista de variables de una sola letra (segundo argumento):

def table( x, v , w = "" ):
   if( v == "" ):
      print( "%s : %d " % ( w, eval( x.replace( "v", " or " ).replace( "~", " ! " ).replace( "+", " and " ))))
   else:
      table( x.replace( v[ 0 ], "0" ), v[ 1 : ], w + "0" )
      table( x.replace( v[ 0 ], "1" ), v[ 1 : ], w + "1" )

por ejemplo

table( "(A v B ) + ~ C", "ABC" )

produce

000 : 0 
001 : 0 
010 : 1 
011 : 0 
100 : 1 
101 : 0 
110 : 1 
111 : 0 

Para obtener su respuesta, evalúe

X = "((A v B) + (~A v ~B)) v ((C v D) + (~C v ~D)) v ((E v F) + (~E v ~F)) v ((G v H) + (~G v ~H)) v ((I v J) + (~I v ~J)) v ((K v L) + (~K v ~L)) v ((M v N) + (~M v ~N)) v ((P v Q) + (~P v ~Q))"
table( X, "ABCDEFGHIJKLMNPQ" )

Aquí hay un módulo de Python que usa una notación diferente para las expresiones booleanas. Es la notación utilizada en enlace donde hay un AND implícito entre variables adyacentes, + significa OR y una comilla simple final ' invierte lo que venga después. Entonces, (A v B ) + ~ C en el ejemplo de Wouter se escribiría como (a + b)c'

Para imprimir la tabla de verdad de la expresión, llame al módulo como:

>>> printtruth("(a+b)c'")
a b c F
0 0 0 0
0 0 1 0
0 1 0 1
0 1 1 0
1 0 0 1
1 0 1 0
1 1 0 1
1 1 1 0

El propio módulo:

def parsebool(s):
    tokens = list()
    allvars = set()
    paridx = list()
    lastpar = None
    for i, char in enumerate(s):
        if char == "'":
            if len(tokens) == 0:
                raise ValueError("cannot negate empty expression")
            elif tokens[-1] == ")":
                tokens.insert(lastpar, "not")
            else:
                tokens.insert(-1, "not")
        elif char == "(":
            if tokens and not (tokens[-1] in ("or", "and", "(")):
                # implicit and
                tokens.append("and")
            paridx.append(len(tokens))
            tokens.append("(")
        elif char == ")":
            tokens.append(")")
            lastpar = paridx.pop()
        elif char.islower() or char == '0' or char == '1':
            if tokens and not (tokens[-1] in ("or", "and", "(")):
                # implicit and
                tokens.append("and")
            if char.islower():
                allvars.add(char)
            tokens.append(char)
        elif char == "+":
            tokens.append("or")
        elif char == "*":
            tokens.append("and")
        elif char in " \t\n":
            pass
        else:
            raise ValueError("invalid character in input: \"%s\"", char)
    return tokens, allvars

def boolfunc(s, name="F"):
    tokens, allvars = parsebool(s)
    allvars = list(sorted(allvars))
    lambdastr = "lambda %s: %s" % (','.join(allvars), ' '.join(tokens))
    F = eval(lambdastr, {'__builtins__':None}, {})
    F.func_doc = 'Boolean function %s(%s) = %s' % (name, ', '.join(allvars), s)
    F.func_name = name
    return F

def printtruth(F):
    if not callable(F):
        F = boolfunc(F)

    varnames = F.func_code.co_varnames
    Fname = F.func_name
    allnames = varnames + (Fname,)
    rowfmt = " ".join("%% %ds" % len(v) for v in allnames)
    print " ".join(allnames)
    for args in itertools.product((0,1), repeat=len(varnames)):
        try:
            result = str(int(F(*args)))
        except Exception:
            result = "E"
        print rowfmt % (args + (result,))

def printcompare(F, G):
    if not callable(F):
        F = boolfunc(F)
    if not callable(G):
        G = boolfunc(G)

    Fvarnames = F.func_code.co_varnames
    Fname = F.func_name
    Gvarnames = G.func_code.co_varnames
    Gname = G.func_name

    varnames = tuple(sorted(frozenset(Fvarnames).union(Gvarnames)))
    allnames = varnames + (Fname, Gname, "=")
    rowfmt = " ".join("%% %ds" % len(v) for v in allnames)
    print " ".join(allnames)

    allequals = True
    for args in itertools.product((0,1), repeat=len(varnames)):
        argdict = dict(zip(varnames, args))
        Fargs = [argdict[n] for n in Fvarnames]
        Gargs = [argdict[n] for n in Gvarnames]
        try:
            Fresult = str(int(F(*Fargs)))
        except Exception:
            Fresult = "E"
        try:
            Gresult = str(int(G(*Gargs)))
        except Exception:
            Gresult = "E"
        equals = Fresult == Gresult
        allequals = allequals and equals
        print rowfmt % (args + (Fresult,Gresult,equals))

    if allequals:
        print "functions are equivalent"
    else:
        print "functions are NOT EQUIVALENT"