convert to CNF/DNF from any simple sentence

等着看《让子弹飞》，激动得写了个小程序，把任何不含“非”的简单句子转换成CNF或DNF范式
其实只做了一件事：把AND和OR按照交换律不断展开
import itertools

def is_leaf(x):
    return type(x)==type("")

def to_str(x):
    return is_leaf(x) and x or "(" + (" "+x[0]+" ").join(map(lambda e : to_str(e), x[1:])) + ")"

def _nfy(x, O1, O2):
    if is_leaf(x):   return x
    if x[0]==O1:  return melt([O1] + map(lambda e : _nfy(e, O1, O2), x[1:]))
    return melt([O1] + [[O2]+list(c) for c in itertools.product(*map(lambda e : is_leaf(e) and [e] or _nfy(e, O1, O2)[1:], x[1:]))])
       
def cnfy(x): return _nfy(x, "AND", "OR")

def dnfy(x): return _nfy(x, "OR", "AND")

def melt(x):
    if is_leaf(x): return x
    ret = x[:1]
    for e in x[1:]:
        if not is_leaf(e) and e[0]==ret[0]:   ret+=melt(e)[1:]
        else:                                 ret.append(melt(e))
    return ret

def main():
    x = ["OR", "a", ["AND", ["OR", "b", ["AND", "c", "d", ["OR", ["AND", "e", "f"], "g", ["OR", ["AND", "h", "i"], "j"]]]], "k"]]
    print to_str(x)
    print to_str(cnfy(x))
    print to_str(dnfy(x))
   
main()

运行结果
(a OR ((b OR (c AND d AND ((e AND f) OR g OR ((h AND i) OR j)))) AND k))
((a OR b OR c) AND (a OR b OR d) AND (a OR b OR e OR g OR h OR j) AND (a OR b OR e OR g OR i OR j) AND (a OR b OR f OR g OR h OR j) AND (a OR b OR f OR g OR i OR j) AND (a OR k))
(a OR (b AND k) OR (c AND d AND e AND f AND k) OR (c AND d AND g AND k) OR (c AND d AND h AND i AND k) OR (c AND d AND j AND k))

参考
First-Order Logic Resolution Theorem Prover In Haskell

更有趣的问题是形式化验证算法的正确性，下回分解