Basic CNF.
2 Name: sml - Simple Modal Logic Lib.
3 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
4 Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
9 # edit your formulae here
14 formula1 = Imp([Eq([p, q]), r])
15 formula2 = Not([Or([p, q])])
16 formula3 = Not([Not([p])])
17 formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])
18 formula5 = Imp([And([Or([p, q]), r]), Not([s])])
19 formula = formula5 # choose your formula here
21 args = parse_arguments()
23 scanner = Scanner(TOKENS)
24 parser = Parser(SYNTAX, scanner)
25 (accepted, out, tree_nodes) = parser.parse(args.formula)
29 tree = SyntaxTree(out, tree_nodes)
33 print "formula: \t\t\t%s [%i]" % (formula, formula.depth())
34 formula = expand_imp_eq(formula)
35 print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth())
36 formula = de_morgan(formula)
37 print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth())
38 formula = reduce_iter(formula)
39 print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth())
40 formula = reduce_iter(dist_mod((formula)))
41 print "distributed modalities+: \t%s [%i]" % (formula, formula.depth())
42 formula = mcnf(formula)
43 print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())
44 cnf_formula = cnf(original)
45 print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
48 return [fun(v) for v in f.values]
50 def expand_imp_eq(formula):
51 expmap = {IMP: lambda (a, b): Or([Not([a]), b]),
52 EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
53 if not isinstance(formula, Operator):
55 if formula.id in expmap:
56 return expmap[formula.id](values(expand_imp_eq, formula))
57 return formula.__class__(values(expand_imp_eq, formula))
59 def de_morgan(formula):
60 negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
61 OR: lambda (a, b): And([negate(a), negate(b)]),
62 BOX: lambda (a,): Diamond([negate(a)]),
63 DIAMOND: lambda (a,): Box([negate(a)]),
64 VARIABLE: lambda (a,): Not([Variable([a])]),
67 return negmap[f.id](f.values)
68 if not isinstance(formula, Operator):
71 return negate(formula.values[0])
72 return formula.__class__(values(de_morgan, formula))
74 def reduce_iter(formula):
75 redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
76 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
78 ids = (formula.id, formula.values[0].id)
80 return reduce_iter(formula.values[0])
81 return formula.__class__(values(reduce_iter, formula))
83 def dist_mod(formula):
84 distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
85 (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
86 (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
87 and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),
88 (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
89 and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}
90 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
92 ids = (formula.id, formula.values[0].id)
94 return distmap[ids](values(dist_mod, formula.values[0]))
95 return formula.__class__(values(dist_mod, formula))
99 conj_id = int(formula.values[1].id == AND)
100 return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]),
101 Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]);
108 sub_formulae.append(v)
110 sub_formulae = [formula]
112 sub_formulae.reverse()
115 for s in sub_formulae:
116 for i, v in enumerate(s.values):
118 s.values[i] = known[v]
119 bicon.append(Eq([Variable(["x" + str(len(bicon))]), s]))
120 known[s] = bicon[-1].values[0]
123 return And([f, conjunct(bicon.pop())])
125 return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
127 """ The Parser - Do NOT look below this line! """
140 class Operator(object):
141 def __init__(self, id, arity, values):
148 if self.id in (BOX, DIAMOND):
149 return 1 + self.values[0].depth()
151 return self.values[0].depth()
152 return max(self.values[0].depth(), self.values[1].depth())
153 def __eq__(self, other):
154 return self.id == other.id and self.values == other.values # commutative types not considered yet
158 out = str(self.values[0])
160 out = self.id + str(self.values[0])
161 elif self.arity == 2:
162 out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
167 def __init__(self, values):
168 Operator.__init__(self, NOT, Not.arity, values)
174 def __init__(self, values):
175 Operator.__init__(self, AND, And.arity, values)
179 def __init__(self, values):
180 Operator.__init__(self, OR, Or.arity, values)
184 def __init__(self, values):
185 Operator.__init__(self, IMP, Imp.arity, values)
189 def __init__(self, values):
190 Operator.__init__(self, EQ, Eq.arity, values)
194 def __init__(self, values):
195 Operator.__init__(self, BOX, Box.arity, values)
197 class Diamond(Operator):
199 def __init__(self, values):
200 Operator.__init__(self, DIAMOND, Diamond.arity, values)
202 class Variable(Operator):
204 def __init__(self, values):
205 Operator.__init__(self, VARIABLE, Variable.arity, values)
209 def __init__(self, values):
210 Operator.__init__(self, LB, Lb.arity, values)
214 def __init__(self, values):
215 Operator.__init__(self, RB, Rb.arity, values)
217 class Formula(object):
221 TOKENS = {re.compile("\("): Lb,
222 re.compile("\)"): Rb,
223 re.compile("~"): Not,
224 re.compile("&"): And,
225 re.compile("\|"): Or,
226 re.compile("->"): Imp,
227 re.compile("<->"): Eq,
228 re.compile("\[\]"): Box,
229 re.compile("<>"): Diamond,
230 re.compile("[a-z]+"): Variable}
232 class Scanner(object):
233 def __init__(self, tokens, source=None):
237 while self.i < len(self.source):
239 for p, token in self.tokens.iteritems():
240 m = p.match(self.source[self.i:])
244 return (token, value)
247 def reset(self, source):
262 SYNTAX = ((Variable,),
273 def __init__(self, parent, value):
277 def addChild(self, value):
278 self.children.append(self, node)
280 class Parser(object):
281 def __init__(self, syntax, scanner):
283 self.scanner = scanner
284 def parse(self, source):
285 table = {(S, Variable): 0,
294 (A, Variable, And): 5,
295 (A, Variable, Or): 6,
296 (A, Variable, Imp): 7,
297 (A, Variable, Eq): 8,
298 (A, Not, Variable, And): 5,
299 (A, Not, Variable, Or): 6,
300 (A, Not, Variable, Imp): 7,
301 (A, Not, Variable, Eq): 8}
306 self.scanner.reset(source)
307 (token, value) = self.scanner.next()
308 (lookahead, la_value) = self.scanner.next()
309 (lookahead2, la2_value) = self.scanner.next()
311 while token and len(stack):
314 tree_nodes.append((token, value))
316 #tree_nodes.append((stack.pop(), value))
317 (token, value) = (lookahead, la_value)
318 (lookahead, la_value) = (lookahead2, la2_value)
319 #(lookahead, _) = self.scanner.next()
320 (lookahead2, la2_value) = self.scanner.next()
323 if (top, token) in table:
324 action = table[(top, token)]
325 elif (top, token, lookahead) in table:
326 action = table[(top, token, lookahead)]
327 elif (top, token, lookahead, lookahead2) in table:
328 action = table[(top, token, lookahead, lookahead2)]
335 stack.extend(reversed(self.syntax[action]))
336 accepted = accepted and not len(stack)
337 return (accepted, out, tree_nodes)
339 class SyntaxTree(object):
340 def __init__(self, seq, tree_nodes):
343 self.root = self.compile(seq, tree_nodes)[0]
344 def compile(self, seq, tree_nodes):
349 c, v = tree_nodes.pop()
351 c, v = tree_nodes.pop()
352 stack.append(Variable(v))
354 stack.append(Not(self.compile(seq, tree_nodes)))
356 stack.extend(self.compile(seq, tree_nodes))
358 stack.append(Box(self.compile(seq, tree_nodes)))
360 stack.append(Diamond(self.compile(seq, tree_nodes)))
362 stack.append(And(self.compile(seq, tree_nodes)))
364 stack.append(Or(self.compile(seq, tree_nodes)))
366 stack.append(Imp(self.compile(seq, tree_nodes)))
368 stack.append(Eq(self.compile(seq, tree_nodes)))
371 from argparse import ArgumentParser
373 def parse_arguments():
374 parser = ArgumentParser(description="Tries to parse simple modal logic syntax and reduces the formula. Edit your formula directly in the code file for best results.")
375 parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't")
376 return parser.parse_args()
378 EXCUSE = """The formula was not accepted by me, because I do not like you. It is not personal. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
380 if __name__ == "__main__":