[PYTHON] Ich habe versucht, einen automatischen Nachweis der Sequenzberechnung zu implementieren

Dieser Artikel wurde am 21. Tag des ISer Adventskalenders 2019 verfasst.

Einführung

In diesem Artikel implementieren wir einen automatischen Beweis unter Verwendung einer Sequenzberechnung der klassischen Aussagenlogik namens G3C. Ich werde mich jedoch auf die Implementierung konzentrieren, ohne zu weit in die strenge Theorie zu gehen. Was Sie in diesem Artikel machen, ist zum Beispiel $ \lnot P \lor Q \Rightarrow P \to Q Wenn Sie die Folge von $ als Eingabe angeben Es wird ein Proof-Diagramm wie dieses ausgegeben. Es gibt verschiedene andere Beweissysteme als die Sequenzberechnung, aber die Sequenzberechnung ist als einfache Möglichkeit bekannt, einen solchen automatischen Beweis durchzuführen. Deshalb werde ich diesmal versuchen, dies umzusetzen.

Was ist Sequenzberechnung?

Reihenfolge

Eine Sequenz ist einfach ein Satz. Zum Beispiel $ A,B \Rightarrow C,D $ Die Sequenz stellt den Satz dar, dass "wenn A und B beide ** wahr sind, dann ist mindestens eines von C und D ** wahr". Wenn dieser Satz richtig ist, werden wir sagen, dass diese Sequenz ** Totologie ** ist.

Beispielsweise kann die folgende Sequenz als Totologie bezeichnet werden. $ A \to B \Rightarrow \lnot A, B $ Wenn "B wenn A" wahr ist, dann gilt "nicht A" oder "ist B". Der Grund dafür ist, dass es mit dem Beweissystem der Sequenzberechnung bewiesen werden kann. Viele Leute mögen denken, dass dieser Satz intuitiv korrekt ist, aber das Beweissystem für die Sequenzberechnung ist so konzipiert, dass es einer solchen Intuition nicht widerspricht.

Logisches Symbol

Im vorherigen Satz wurden $ \ lnot $ und $ \ to $ als logische Symbole ausgegeben. In der Aussagenlogik gibt es nur vier Arten von logischen Symbolen. Sie entsprechen der intuitiven Bedeutung.

Symbol	Beispiel	Bedeutung
\lnot	\lnot A	Kein
\land	A\land B	A und B
\lor	A\lor B	A oder B
\to	A \to B	Wenn A, dann B.

Inferenzregeln

Sie müssen in der Lage sein, einen Beweis zu erbringen. Inferenz wird in der folgenden Form ausgedrückt. $ \cfrac{A \Rightarrow B}{C \Rightarrow D} $ Dies bedeutet, dass, wenn die Sequenz $ A \ Rightarrow B $ eine Totologie ist, die Sequenz $ C \ Rightarrow D $ auch eine Totologie ist, dh $ C \ Rightarrow D $ kann von $ A \ Rightarrow B $ abgeleitet werden.

Die folgenden acht Arten von Inferenzregeln sind im G3C-Proofsystem definiert. Der Beweis wird unter Verwendung dieser acht Arten von Inferenzregeln erstellt. Beachten Sie, dass die Reihenfolge der logischen Ausdrücke auf jeder Seite der Sequenz beliebig geändert werden kann. $ \ cfrac {\ Gamma \ Rightarrow \ Delta, A} {\ lnot A, \ Gamma \ Rightarrow \ Delta} (\ lnot left) \qquad \ cfrac {A, \ Gamma \ Rightarrow \ Delta} {\ Gamma \ Rightarrow \ Delta, \ lnot A} (\ lnot right) $$ \ cfrac {A, B, \ Gamma \ Rechtspfeil \ Delta} {A \ Land B, \ Gamma \ Rechtspfeil \ Delta} (\ Land links) \qquad \ cfrac {\ Gamma \ Rechtspfeil \ Delta, A \ Quad \ Gamma \ Rechtspfeil \ Delta, B} {\ Gamma \ Rechtspfeil \ Delta, A \ Land B} (\ Land rechts) $$ \ cfrac {A, \ Gamma \ Rechtspfeil \ Delta \ Quad B, \ Gamma \ Rechtspfeil \ Delta} {A \ lor B, \ Gamma \ Rechtspfeil \ Delta} (\ lor links) \qquad \ cfrac {\ Gamma \ Rightarrow \ Delta, A, B} {\ Gamma \ Rightarrow \ Delta, A \ lor B} (\ lor right) $$ \ cfrac {\ Gamma \ Rechtspfeil \ Delta, A \ Quad B, \ Gamma \ Rechtspfeil \ Delta} {A \ bis B, \ Gamma \ Rechtspfeil \ Delta} (\ nach links) \qquad \ cfrac {A, \ Gamma \ Rechtspfeil \ Delta, B} {\ Gamma \ Rechtspfeil \ Delta, A \ bis B} (\ nach rechts) $ Diese Inferenzregeln überzeugen intuitiv. Schauen Sie sich zum Beispiel die Inferenz "$ \ lnot $ left" an. Unter der Annahme von $ \ Gamma $ wissen wir nun, dass $ \ Delta $ oder $ A $ gilt.

(i) Wenn $ \ Delta $ von $ \ Gamma $ abgeleitet werden kann, dann ist natürlich $ \ lnot A, \ Gamma \ Rightarrow \ Delta $ wahr. (ii) Wenn $ A $ von $ \ Gamma $ abgeleitet werden kann, dann werden $ \ lnot A und \ Gamma $ niemals wahr sein, so dass $ \ lnot A, \ Gamma \ Rightarrow \ Delta $ unabhängig von der rechten Seite konstant ist. Das ist wahr.

Ich werde nicht über andere Inferenzregeln schreiben, aber ich denke, Sie können überzeugt sein, wenn Sie so denken.

Sequenz starten

Nun werden wir den Beweis durchführen, indem wir die oben genannten Inferenzregeln kombinieren. Zu diesem Zweck benötigen wir jedoch eine Sequenz, die ein Axiom ist, das sich oben im Beweisdiagramm befindet. Dies wird als ** Startsequenz ** bezeichnet. Dies sollte eine Sequenz sein, die selbstverständlich für alle gilt. Die Sequenz, die aus der konstanten Sequenz abgeleitet werden kann, ist ebenfalls konstant.

Die Startsequenz in dem hier behandelten Beweissystem ist nur die in der folgenden Form. $ P,\Gamma \Rightarrow P,\Delta $ Wenn $ P, \ Gamma $ beide wahr sind, dann ist mindestens eines von $ P, \ Delta $ wahr. Es ist natürlich, weil $ P $ wahr ist.

Beweis

Wenn eine zu beweisende Sequenz gegeben ist, wenn die Inferenzregel wiederholt von der Startsequenz angewendet wird und die endgültig zu gebende Sequenz übereinstimmt, ist der Beweis abgeschlossen.

Als Beispiel die erste Sequenz, die ich gegeben habe $ A \to B \Rightarrow \lnot A, B $ Lassen Sie uns nach dieser Regel beweisen. Das Folgende ist der Beweis. Das Ziel dieser Zeit ist es, dieses Proofdiagramm automatisch zu zeichnen.

Proof-Suchalgorithmus

Sequenzgröße

Lassen Sie mich vor der Einführung des Proof-Suchalgorithmus das Konzept der Sequenz ** Größe ** vorstellen. Die Größe ist die Gesamtzahl der logischen Symbole $ \ lnot, \ land, \ lor, \ bis , die in der Sequenz enthalten sind. Zum Beispiel $ A \to B \Rightarrow \lnot A, B $$ Da die Sequenz nacheinander $ \ bis $ und $ \ lnot $ enthält, beträgt die Größe 2.

Schauen wir uns nun noch einmal die Argumentationsregeln an und konzentrieren uns dabei auf die Größe. Sie können sehen, dass in jeder Argumentationsregel die Größe der Sequenz unterhalb der Linie um eins größer ist als die Größe der Sequenz oben. Dies ist der Punkt der Beweissuche.

Sequenz der Größe 0

Da der Beweis im Wesentlichen Schlussfolgerungen aus Entschuldigungen zieht, ist es natürlich, Beweisdiagramme von oben nach unten zu zeichnen. Wenn jedoch bei der Proof-Suche eine zu beweisende Sequenz angegeben wird, wird die Suche von unten nach oben durchgeführt, wobei diese als unten verwendet wird. Wenn Sie dem Proof-Diagramm einen Schritt nach oben folgen, wird die Größe um 1 reduziert. Wenn Sie also die Inferenzregeln wiederholt anwenden, erhalten Sie schließlich eine Reihe von Sequenzen der Größe 0, unabhängig davon, welche Sequenz Sie beweisen müssen. Machen. Eine Sequenz der Größe 0 kann nicht mehr transformiert werden. Sie können also feststellen, ob sie wahr ist, indem Sie nur prüfen, ob es sich um eine Startsequenz handelt.

Algorithmus

Der Proof-Suchalgorithmus wird auch als "Wang-Algorithmus" bezeichnet. Es ist ein schöner Name, aber die Idee ist ganz natürlich. Es gibt nichts Neues. Wenn die gegebene Sequenz auf eine Sequenz der Größe 0 reduziert ist und alle Startsequenzen sind, kann die ursprüngliche Sequenz bewiesen werden, und wenn eine nicht die Startsequenz ist, kann sie nicht bewiesen werden. Ich werde unten im Detail schreiben. Grundsätzlich handelt es sich um einen Algorithmus, der bestimmt, ob eine bestimmte Sequenz eine Totologie ist. Mit ein wenig Einfallsreichtum können Sie jedoch auch ein Beweisdiagramm zeichnen.

Angenommen, Sie erhalten die Sequenz $ \ Gamma \ Rightarrow \ Delta $. Überprüfen Sie zunächst, ob die Größe dieser Sequenz 0 ist. Wenn es 0 ist, können Sie feststellen, ob es sich um eine Totologie handelt, indem Sie bestimmen, ob es sich um eine Anfangssequenz handelt.

Wenn die Größe größer oder gleich 1 ist, enthält $ \ Gamma \ Rightarrow \ Delta $ immer die logischen Symbole $ \ lnot, \ land, \ lor, \ to $. Wenn Sie von links danach suchen und ein logisches Symbol finden, können Sie den Inferenzregeln von unten nach oben folgen, um eine oder zwei Sequenzen zu erhalten, die eine kleinere Größe haben. Stellen Sie auf ähnliche Weise fest, ob diese Sequenzen Totologie sind. Das Wiederholen dieses Vorgangs führt schließlich zu einer Folge der Größe 0, und Sie können rekursiv bestimmen, ob $ \ Gamma \ Rightarrow \ Delta $ eine Totologie ist.

Es ist lange her, aber die Grundidee ist einfach. Wir werden diesen Algorithmus von nun an implementieren.

Implementierung der Proof-Suche

Hier ist es in Python3 implementiert. Ich werde den gesamten Code am Ende dieses Artikels einfügen, aber ich werde nur den wichtigen Teil hier schreiben.

Ziehen Sie in Betracht, drei Klassen zu definieren.

Atomformel
Formel
Sequent
AtomicFormula Es ist ein Satz, der nicht mehr geteilt werden kann, wie $ P, Q $.

class AtomicFormula:
    def __init__(self, name):
        self.name = name
    def is_atomic(self):
        return True

Hat nur einen Namen. is_atomic wird in Zukunft verwendet, also definieren Sie es.

2. Formel

Es gibt verschiedene logische Ausdrücke wie $ P \ bis Q, \ quad \ lnot (S \ land T), \ quad P \ bis ((P \ land Q) \ lor (S \ land T)) $. , Konzentration auf seine hierarchische Struktur, auf der äußersten Seite

\lnot A
A\land B
A\lor B
A\to B Sie können sehen, dass es eine der Formen hat. Definieren Sie basierend darauf.

class Formula:
    def __init__(self, relation, form1, form2=None):
        self.relation = relation
        self.form1 = form1
        self.form2 = form2
    def is_atomic(self):
        return False

self.relation wird für $ \ lnot, \ land, \ lor, \ to $ auf 1,2,3,4 gesetzt. Definieren Sie außerdem "is_atomic" mit $ A $ als "form1" und $ B $ als "form2".

3. Sequent

Die Sequenz enthält Spalten mit logischen Ausdrücken links und rechts von $ \ Rightarrow $. Die Proof-Diagramm-Suche ist als Methode dieser Klasse definiert.

class Sequent:
    def __init__(self, Left, Right):
        self.Left = Left
        self.Right = Right  #Left,Richtig ist die Formel,Liste der Atomformeln
    #Sequenzbeurteilung starten
    def is_initial(self):
        for l in self.Left:
            if l in self.Right: return True
        return False
    #Sequentielle Beurteilung der Größe 0
    def is_atomic(self):
        for l in self.Left:
            if not l.is_atomic(): return False
        for r in self.Right:
            if not r.is_atomic(): return False
        return True
    #Thothologisches Urteil
    def is_tautology(self):
        if self.is_atomic():
            return self.is_initial()
           
        for l in range(len(self.Left)):
            if not self.Left[l].is_atomic():
                self.Left[0],self.Left[l]=self.Left[l],self.Left[0]
                form = self.Left[0]
                if form.relation==1:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).is_tautology()
                if form.relation==2:
                    return Sequent(self.Left[1:]+[form.form1,form.form2], self.Right).is_tautology()
                if form.relation==3:
                    return Sequent(self.Left[1:]+[form.form1], self.Right).is_tautology() and Sequent(self.Left[1:]+[form.form2], self.Right).is_tautology()
                if form.relation==4:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).is_tautology() and Sequent(self.Left[1:]+[form.form2], self.Right).is_tautology()
        
        for r in range(len(self.Right)):
            if not self.Right[r].is_atomic():
                self.Right[0],self.Right[r]=self.Right[r],self.Right[0]
                form=self.Right[0]
                if form.relation==1:
                    return Sequent(self.Left+[form.form1], self.Right[1:]).is_tautology()
                if form.relation==2:
                    return Sequent(self.Left, self.Right[1:]+[form.form1]).is_tautology() and Sequent(self.Left, self.Right[1:]+[form.form2]).is_tautology()
                if form.relation==3:
                    return Sequent(self.Left, self.Right[1:]+[form.form1,form.form2]).is_tautology()
                if form.relation==4:
                    return Sequent(self.Left+[form.form1], self.Right[1:]+[form.form2]).is_tautology()

    def prooftree(self):
        #ich schreibe später

is_tautology implementiert Wangs Algorithmus und Inferenzregeln so wie sie sind. Wenn das erste Element von "Links", "Rechts" atomar ist, wird es durch ein nichtatomares Element ersetzt, und die Inferenzregel wird auf das erste Element angewendet.

Jetzt können Sie feststellen, ob dies bewiesen werden kann, indem Sie die Methode "is_tautology" für eine beliebige Sequenz aufrufen. Übrigens in dieser Definition zum Beispiel $ A \to B \Rightarrow \lnot A, B $ Ist

Sequent([Formula(4, AtomicFormula('A'), AtomicFormula('B'))], [Formula(1, AtomicFormula('A')), AtomicFormula('B')])

Bitte beachten Sie, dass es als dargestellt wird. Der Code, der diese Konvertierung durchführt, wird verschoben.

Fahren wir nun mit "prooftree" fort, der Methode zum Zeichnen eines Proofdiagramms. Wir werden jedoch die Prooftree-Umgebung von LaTeX verwenden, um das Proofdiagramm zu schreiben. Es ist einfach zu bedienen, daher sollten Sie sich [diese Site] ansehen (http://kivantium.hateblo.jp/entry/2015/04/07/103802). Die Methode "prooftree" wird erstellt, um den Code zurückzugeben, der an diese Umgebung übergeben werden soll.

Schreiben Sie in dieser Umgebung so viel, wie Sie einen Zweig des Proof-Diagramms schreiben können. Wenn Sie ihn nicht schreiben können, wechseln Sie zu einem anderen Zweig und integrieren Sie ihn. Was ich sagen möchte ist, dass ich das Proof-Diagramm in der genau umgekehrten Reihenfolge der Proof-Suche schreibe. Diese Tatsache macht es sehr einfach, ein Beweisdiagramm zu zeichnen. Sie müssen im Verlauf der Erkundung immer mehr hinzufügen. Das Folgende ist die Definition von "Proof Tree", die fast mit "is_tautology" identisch ist.

def prooftree(self):
        if self.is_atomic(): return '\\AxiomC'+str(self)
        string = str(self)
        for l in range(len(self.Left)):
            if not self.Left[l].is_atomic():
                self.Left[0],self.Left[l]=self.Left[l],self.Left[0]
                form = self.Left[0]
                if form.relation==1:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==2:
                    return Sequent(self.Left[1:]+[form.form1,form.form2], self.Right).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==3:
                    return Sequent(self.Left[1:]+[form.form1], self.Right).prooftree() + Sequent(self.Left[1:]+[form.form2], self.Right).prooftree() +'\n'+'\\BinaryInfC'+string
                if form.relation==4:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).prooftree() + Sequent(self.Left[1:]+[form.form2], self.Right).prooftree() + '\n'+'\\BinaryInfC'+string
        
        for r in range(len(self.Right)):
            if not self.Right[r].is_atomic():
                self.Right[0],self.Right[r]=self.Right[r],self.Right[0]
                form=self.Right[0]
                if form.relation==1:
                    return Sequent(self.Left+[form.form1], self.Right[1:]).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==2:
                    return Sequent(self.Left, self.Right[1:]+[form.form1]).prooftree() + Sequent(self.Left, self.Right[1:]+[form.form2]).prooftree()+'\n'+'\\BinaryInfC'+string
                if form.relation==3:
                    return Sequent(self.Left, self.Right[1:]+[form.form1,form.form2]).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==4:
                    return Sequent(self.Left+[form.form1], self.Right[1:]+[form.form2]).prooftree()+'\n'+'\\UnaryInfC'+string

Definieren Sie abschließend eine Funktion, die einen logischen Ausdruck (keine Sequenz), der mit $ \ lnot, \ land, \ lor, \ to $ geschrieben wurde, in verschachtelte Klassen konvertiert. Da es einfach ist, die Sequenz in logische Ausdrücke zu unterteilen, werde ich sie weglassen. Es wird angenommen, dass $ \ lnot $ die höchste Priorität für logische Symbole hat und dass alles andere gleichwertig ist. Die Implementierung versucht irgendwie, die logischen Symbole der äußersten Hierarchie zu finden.

def read(exp):
    if '¬' in exp or '∧' in exp or '∨' in exp or '→' in exp:
        #()Suchen Sie das logische Symbol außerhalb von
        i=len(exp)-1
        if exp[i]==')':
            c=1
            while c:
                i-=1
                if exp[i]=='(': c-=1
                elif exp[i]==')': c+=1
            if i==0:
                return read(exp[1:-1])
            
        while exp[i] not in ['∧' , '∨' , '→']:
            if i==0 and exp[i]=='¬':
                return Formula(1, read(exp[1:]))
            i-=1
        if exp[i]=='∧': return Formula(2, read(exp[:i]), read(exp[i+1:]))
        elif exp[i]=='∨': return Formula(3, read(exp[:i]), read(exp[i+1:]))
        elif exp[i]=='→': return Formula(4, read(exp[:i]), read(exp[i+1:]))
                    
    return AtomicFormula(exp)

Es ist lange her, aber die Implementierung ist vorbei. Am Ende wird der gesamte Code veröffentlicht. Geben Sie daher verschiedene Sequenzen ein und probieren Sie ihn aus.

Am Ende

Vielen Dank, dass Sie so weit gelesen haben. Ich denke, es gab einen Teil der Erklärung, der im ersten Artikel unfreundlich war. Die Beschreibung kann an einigen Stellen ungenau sein. Ich würde es begrüßen, wenn Sie auf verschiedene Dinge hinweisen könnten. Der Code, den ich dieses Mal geschrieben habe, umfasst insgesamt weniger als 200 Zeilen. Ich denke, Sie können sehen, dass Sie mithilfe der Sequenzberechnung auf einfache Weise einen automatischen Proof erstellen können. Natürlich kann es durch andere Methoden automatisiert werden, daher kann es interessant sein, es mit natürlichen Leistungen zu versuchen. Dann werde ich den gesamten Code am Ende setzen.

Alle Codes

# -*- coding: utf-8 -*-

import sys

class AtomicFormula:
    
    def __init__(self, name):
        self.name = name
        
    def is_atomic(self):
        return True
    
    def __eq__(self, other):
        if type(other) != AtomicFormula: return False
        return self.name == other.name
    
    def __str__(self):
        return self.name
        
        
class Formula:
    
    def __init__(self, relation, form1, form2=None):
        self.relation = relation
        # 1:not
        # 2:and
        # 3:or
        # 4:->
        self.form1 = form1
        self.form2 = form2
            
    def is_atomic(self):
        return False
    
    def __eq__(self, other):
        if type(other) != Formula: return False
        return self.relation==other.relation and self.form1==other.form1 and self.form2==other.form2
    
    def __str__(self):
        if self.relation==1: return '\\lnot '+str(self.form1)
        if self.relation==2: return '('+str(self.form1)+'\\land '+str(self.form2)+')'
        if self.relation==3: return '('+str(self.form1)+'\\lor '+str(self.form2)+')'
        if self.relation==4: return '('+str(self.form1)+'\\to '+str(self.form2)+')'

    
class Sequent:
    
    def __init__(self, Left, Right):
        self.Left = Left
        self.Right = Right
        
    def is_initial(self):
        for l in self.Left:
            if l in self.Right: return True
        return False
    
    def is_atomic(self):
        for l in self.Left:
            if not l.is_atomic(): return False
        for r in self.Right:
            if not r.is_atomic(): return False
        return True
    
    def is_tautology(self):
        if self.is_atomic():
            return self.is_initial()
           
        for l in range(len(self.Left)):
            if not self.Left[l].is_atomic():
                self.Left[0],self.Left[l]=self.Left[l],self.Left[0]
                form = self.Left[0]
                if form.relation==1:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).is_tautology()
                if form.relation==2:
                    return Sequent(self.Left[1:]+[form.form1,form.form2], self.Right).is_tautology()
                if form.relation==3:
                    return Sequent(self.Left[1:]+[form.form1], self.Right).is_tautology() and  Sequent(self.Left[1:]+[form.form2], self.Right).is_tautology()
                if form.relation==4:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).is_tautology() and Sequent(self.Left[1:]+[form.form2], self.Right).is_tautology()
        
        for r in range(len(self.Right)):
            if not self.Right[r].is_atomic():
                self.Right[0],self.Right[r]=self.Right[r],self.Right[0]
                form=self.Right[0]
                if form.relation==1:
                    return Sequent(self.Left+[form.form1], self.Right[1:]).is_tautology()
                if form.relation==2:
                    return Sequent(self.Left, self.Right[1:]+[form.form1]).is_tautology() and Sequent(self.Left, self.Right[1:]+[form.form2]).is_tautology()
                if form.relation==3:
                    return Sequent(self.Left, self.Right[1:]+[form.form1,form.form2]).is_tautology()
                if form.relation==4:
                    return Sequent(self.Left+[form.form1], self.Right[1:]+[form.form2]).is_tautology()
         
    def prooftree(self):
        if self.is_atomic(): return '\\AxiomC'+str(self)
        string = str(self)
        for l in range(len(self.Left)):
            if not self.Left[l].is_atomic():
                self.Left[0],self.Left[l]=self.Left[l],self.Left[0]
                form = self.Left[0]
                if form.relation==1:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==2:
                    return Sequent(self.Left[1:]+[form.form1,form.form2], self.Right).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==3:
                    return Sequent(self.Left[1:]+[form.form1], self.Right).prooftree() + Sequent(self.Left[1:]+[form.form2], self.Right).prooftree() +'\n'+'\\BinaryInfC'+string
                if form.relation==4:
                    return Sequent(self.Left[1:], self.Right+[form.form1]).prooftree() + Sequent(self.Left[1:]+[form.form2], self.Right).prooftree() + '\n'+'\\BinaryInfC'+string
        
        for r in range(len(self.Right)):
            if not self.Right[r].is_atomic():
                self.Right[0],self.Right[r]=self.Right[r],self.Right[0]
                form=self.Right[0]
                if form.relation==1:
                    return Sequent(self.Left+[form.form1], self.Right[1:]).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==2:
                    return Sequent(self.Left, self.Right[1:]+[form.form1]).prooftree() + Sequent(self.Left, self.Right[1:]+[form.form2]).prooftree()+'\n'+'\\BinaryInfC'+string
                if form.relation==3:
                    return Sequent(self.Left, self.Right[1:]+[form.form1,form.form2]).prooftree()+'\n'+'\\UnaryInfC'+string
                if form.relation==4:
                    return Sequent(self.Left+[form.form1], self.Right[1:]+[form.form2]).prooftree()+'\n'+'\\UnaryInfC'+string
            
    def __str__(self):
        return '{$'+','.join(map(str,self.Left))+'\Rightarrow '+','.join(map(str,self.Right))+'$}'

def read(exp):
    if '¬' in exp or '∧' in exp or '∨' in exp or '→' in exp:
        #()Suchen Sie das logische Symbol außerhalb von
        i=len(exp)-1
        if exp[i]==')':
            c=1
            while c:
                i-=1
                if exp[i]=='(': c-=1
                elif exp[i]==')': c+=1
            if i==0:
                return read(exp[1:-1])
            
        while exp[i] not in ['∧' , '∨' , '→']:
            if i==0 and exp[i]=='¬':
                return Formula(1, read(exp[1:]))
            i-=1
        if exp[i]=='∧': return Formula(2, read(exp[:i]), read(exp[i+1:]))
        elif exp[i]=='∨': return Formula(3, read(exp[:i]), read(exp[i+1:]))
        elif exp[i]=='→': return Formula(4, read(exp[:i]), read(exp[i+1:]))
                    
    return AtomicFormula(exp)

while True:
    try:
        exp = input("Sequent> ").replace(' ','')
        if exp=="exit": sys.exit()
        left , right = exp.split('⇒')
        seq = Sequent(list(map(read, left.split(','))), (list(map(read, right.split(',')))))
        if seq.is_tautology():
            print(seq.prooftree())
        else:
            print("Not Provable")
    except EOFError:
        sys.exit()
    except (AttributeError, ValueError):
        print("Error: Invalid Input")