#!/usr/bin/env python2.7 # ---------------------------------- # # Module tableaux.py """ This module implements the propositional tableaux-calculus in a straightforward manner. Copyright 2011,2015 Stephan Schulz, schulz@eprover.org This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program ; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA The original copyright holder can be contacted as Stephan Schulz Auf der Altenburg 7 70376 Stuttgart Germany Email: schulz@eprover.org """ import unittest import sys import getopt from lexer import Lexer, Token from prop_formula import PropFormula, parseFormula class Tableaux(object): """ A class representing a tableaux node. It contains pointers to parents and children, formula, and two states (open and closed, new and expanded). """ tNodeCounter = 0 def __init__(self, formula): self.parent = None self.children = None self.formula = formula self.closed = False self.expanded = False self.nodeId = Tableaux.tNodeCounter Tableaux.tNodeCounter = Tableaux.tNodeCounter+1 def nodeStr(self): return "tn%ld"%(self.nodeId,) def nodeXStr(self): return "tn%ld: %s"%(self.nodeId,str(self.formula)) def __str__(self): expanded = "" closed = "" if self.closed: if self.isLeaf(): closed = "
(X)" if self.expanded: expanded = " ✓" label = " [label=<%s%s%s>]\n"%(str(self.formula),expanded,closed) res = self.nodeStr()+label if self.children: for l in self.children: res = res+" %s -- %s\n"%(self.nodeStr(), l.nodeStr()) elif self.closed: res = res+" %s -- %s [color=red style=dashed weight=0.001]\n"%\ (self.nodeStr(), self.closed.nodeStr()) return res def rekStr(self): """ Return a string representation of the complete tree as a list of node descriptions. """ res = [self.__str__()] if self.children: for l in self.children: res.extend(l.rekStr()) return res def addParent(self, parent): self.parent = parent def addChildren(self, children): self.children = children def isLeaf(self): return self.children == None def getOpenLeaves(self): """ Return a list of all leaves under self. """ if self.closed: return [] if self.isLeaf(): return [self] res = [] for c in self.children: res.extend(c.getOpenLeaves()) return res def checkClosed(self): """ Check if self closes the path to self. If yes, store complementary node. """ node = self.parent while node: if node.formula.isComplement(self.formula): self.closed = node break node = node.parent return self.closed def propagateClosed(self): if not self.closed and self.children: self.closed = True for c in self.children: if not c.closed: self.closed = False break if self.closed and self.parent: self.parent.propagateClosed() def alphaExtend(self, formulas): """ Extend the leaf with the alpha-subformula in formulas. Return all newly created nodes. """ assert self.isLeaf() if not formulas or self.closed: return [] form = formulas[0] newnode = Tableaux(form) self.addChildren([newnode]) newnode.addParent(self) newnode.checkClosed() res = [newnode] res.extend(newnode.alphaExtend(formulas[1:])) return res def betaExtend(self, formulas): """ Extend the leaf with the beta-subformula in formulas. Return all newly created leaves. """ assert self.isLeaf() if not formulas or self.closed: return [] res = [] for f in formulas: newnode = Tableaux(f) newnode.addParent(self) newnode.checkClosed() res.append(newnode) self.addChildren(res) return res class TableauxProof(object): """ A class to represent a tableaux-proof in construction. It contains the tableaux proper, plus auxilliary information """ def __init__(self, formula): """ Initialize the formula. """ self.tableau = Tableaux(formula) self.openalphalist = [self.tableau] self.openbetalist = [] def nextNode(self): if self.openalphalist: return self.openalphalist.pop() return self.openbetalist.pop() def hasOpenNodes(self): return self.openalphalist or self.openbetalist def step(self): node = self.nextNode() print "# Expanding node:", node.nodeXStr() node.expanded = True leaves = node.getOpenLeaves() if not leaves: return newnodes = [] split = node.formula.alphaSplit() if split: for l in leaves: newnodes.extend(l.alphaExtend(split)) else: split = node.formula.betaSplit() if split: for l in leaves: newnodes.extend(l.betaExtend(split)) for node in newnodes: if not node.checkClosed(): if node.formula.isAlpha(): self.openalphalist[0:0] = [node] elif node.formula.isBeta(): self.openbetalist[0:0] = [node] else: node.propagateClosed() def proof(self): global stepCount, printSteps if printSteps: fp = open("%s%03d.gv"%(printSteps,stepCount), "w") fp.write(self.__str__()+"\n") fp.close() while self.hasOpenNodes(): self.step() stepCount = stepCount+1 if printSteps: fp = open("%s%03d.gv"%(printSteps,stepCount), "w") fp.write(self.__str__()+"\n") fp.close() def isClosed(self): return self.tableau.closed def __str__(self): """ Return a printable representation of the tableaux in DOT format. """ res = ["graph TableauxProof{\n node[shape=plaintext]\n ranksep=0.2\n"] res.extend(self.tableau.rekStr()) res.append("}") return "\n".join(res) class TestTableaux(unittest.TestCase): """ Test the lexer functions. """ def setUp(self): print self.example1 = "(p & (~ (q->p))) (p & (q->p))" lex = Lexer(self.example1) self.f1 = parseFormula(lex) self.f2 = parseFormula(lex) def testTableau(self): tnode = Tableaux(self.f1) print tnode proof = TableauxProof(self.f2) print proof alphas = proof.tableau.formula.alphaSplit() proof.tableau.alphaExtend(alphas) betas = proof.tableau.children[0].formula.betaSplit() print "Beta:", proof.tableau.children[0] print betas proof.tableau.betaExtend(betas) def testRules(self): proof = TableauxProof(self.f1) while proof.openlist: print "Main loop" proof.step() print proof def processOptions(opts): """ Process the options given. The only one so far is to run unit tests. By default, read and print back a set of arithmetic expressions. """ global printProofs, checkTaut, printSteps for opt, optarg in opts: if opt == "-u" or opt == "--unit-tests": # Unit tests don't like options sys.argv = [sys.argv[0]] unittest.main() sys.exit() elif opt == "-p" or opt == "--proof": printProofs = True elif opt == "-t" or opt == "--check-tautology": checkTaut = True elif opt == "-s" or opt == "--print-steps": printSteps = optarg if __name__ == '__main__': printProofs = False checkTaut = False printSteps = False stepCount = 0 opts, args = getopt.gnu_getopt(sys.argv[1:], "upts:", ["unit-tests", "proof", "check-tautology", "print-steps="]) processOptions(opts) for file in args: fp = open(file, "r") input = fp.read() fp.close() lex = Lexer(input) while(not lex.TestTok(Token.EOFToken)): expr = parseFormula(lex) if not checkTaut: t = TableauxProof(expr) t.proof() if t.isClosed(): print "# ", expr, "is unsatisfiable" else: print "# ", expr, "is satisfiable" else: nexpr = expr.negation() t = TableauxProof(nexpr) t.proof() if t.isClosed(): print "# ", expr, "is a tautology" else: print "# ", expr, "is not a tautology" if printProofs: print t