J'ai essayé d'implémenter le calcul automatique de la preuve de séquence

Cet article a été écrit comme le 21e jour du Calendrier de l'Avent ISer 2019.

introduction

Dans cet article, nous allons implémenter une preuve automatique en utilisant un calcul séquentiel de logique propositionnelle classique appelé G3C. Cependant, je me concentrerai sur la mise en œuvre sans aller trop loin dans la théorie rigoureuse. Ce que vous faites dans cet article est, par exemple, $ \lnot P \lor Q \Rightarrow P \to Q Si vous donnez la séquence de $ comme entrée Il produira un diagramme de preuve comme celui-ci. Il existe plusieurs systèmes de preuve autres que le calcul de séquence, mais le calcul de séquence est connu pour rendre une telle preuve automatique facile. Par conséquent, je vais essayer de mettre en œuvre cela cette fois.

Qu'est-ce que le calcul de séquence?

Séquence

Une séquence est simplement une proposition. Par exemple $ A,B \Rightarrow C,D $ La séquence représente la proposition que «si A et B sont tous les deux ** vrais, alors au moins un de C et D est ** vrai». Lorsque cette proposition est correcte, nous dirons que cette séquence est ** totologie **.

Par exemple, la séquence suivante peut être considérée comme une totologie. $ A \to B \Rightarrow \lnot A, B $ Si "B si A" est vrai, alors "pas A" ou "est B" est valable. La raison pour laquelle il est vrai est qu'il peut être prouvé en utilisant le système de preuve du calcul séquentiel. Beaucoup de gens peuvent penser que cette proposition est intuitivement correcte, mais le système de preuve pour le calcul séquentiel est conçu pour ne pas aller à l'encontre d'une telle intuition.

Symbole logique

Dans la proposition précédente, $ \ lnot $ et $ \ to $ sont sortis comme des symboles logiques. Il n'y a que quatre types de symboles logiques dans la logique propositionnelle. Ils correspondent à la signification intuitive.

symbole	Exemple	sens
\lnot	\lnot A	Pas un
\land	A\land B	A et B
\lor	A\lor B	A ou B
\to	A \to B	Si A, alors B

Règles d'inférence

Vous devez être capable de déduire pour faire une preuve. L'inférence est exprimée sous la forme suivante. $ \cfrac{A \Rightarrow B}{C \Rightarrow D} $ Cela signifie que si la séquence $ A \ Rightarrow B $ est une totologie, alors la séquence $ C \ Rightarrow D $ est aussi une totologie, c'est-à-dire que $ C \ Rightarrow D $ peut être dérivé de $ A \ Rightarrow B $.

Les huit types de règles d'inférence suivants sont définis dans le système de preuve G3C. La preuve sera construite en utilisant ces huit types de règles d'inférence. Notez que l'ordre des expressions logiques peut être modifié arbitrairement de chaque côté de la séquence. $ \ 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 \ Rightarrow \ Delta} {A \ land B, \ Gamma \ Rightarrow \ Delta} (\ land gauche) \qquad \ cfrac {\ Gamma \ Rightarrow \ Delta, A \ quad \ Gamma \ Rightarrow \ Delta, B} {\ Gamma \ Rightarrow \ Delta, A \ land B} (\ land right) $$ \ cfrac {A, \ Gamma \ Rightarrow \ Delta \ quad B, \ Gamma \ Rightarrow \ Delta} {A \ lor B, \ Gamma \ Rightarrow \ Delta} (\ lor left) \qquad \ cfrac {\ Gamma \ Rightarrow \ Delta, A, B} {\ Gamma \ Rightarrow \ Delta, A \ lor B} (\ lor right) $$ \ cfrac {\ Gamma \ Rightarrow \ Delta, A \ quad B, \ Gamma \ Rightarrow \ Delta} {A \ to B, \ Gamma \ Rightarrow \ Delta} (\ à gauche) \qquad \ cfrac {A, \ Gamma \ Rightarrow \ Delta, B} {\ Gamma \ Rightarrow \ Delta, A \ à B} (\ à droite) $ Ces règles d'inférence sont intuitivement convaincantes. Par exemple, jetez un œil à l'inférence "$ \ lnot $ left". Maintenant, en supposant $ \ Gamma $, nous savons que $ \ Delta $ ou $ A $ tient.

(i) Si $ \ Delta $ peut être dérivé de $ \ Gamma $, alors bien sûr $ \ lnot A, \ Gamma \ Rightarrow \ Delta $ est vrai. (ii) Si $ A $ peut être dérivé de $ \ Gamma $, alors $ \ lnot A et \ Gamma $ ne seront jamais vrais, donc $ \ lnot A, \ Gamma \ Rightarrow \ Delta $ est constant quel que soit le côté droit. C'est vrai.

Je n'écrirai pas sur les autres règles d'inférence, mais je pense que vous pouvez être convaincu en pensant de cette façon.

Démarrer la séquence

Maintenant, nous allons effectuer la preuve en combinant les règles d'inférence mentionnées ci-dessus, mais pour cela, nous avons besoin d'une séquence qui est un axiome situé en haut du diagramme de preuve. C'est ce qu'on appelle la ** séquence de démarrage **. Cela devrait être une séquence qui est évidemment vraie pour tout le monde. La séquence qui peut être dérivée de la séquence constante est également constante.

La séquence de départ dans le système de preuve dont il est question ici n'est que celle de la forme suivante. $ P,\Gamma \Rightarrow P,\Delta $ Si $ P, \ Gamma $ sont tous les deux vrais, alors au moins un des $ P, \ Delta $ est vrai. C'est naturel parce que $ P $ est vrai.

Preuve

Lorsqu'une séquence à prouver est donnée, si la règle d'inférence est appliquée à plusieurs reprises à partir de la séquence de départ et correspond finalement à la séquence donnée, la preuve est terminée.

A titre d'exemple, la première séquence que j'ai donnée $ A \to B \Rightarrow \lnot A, B $ Prouvons selon cette règle. Ce qui suit en est la preuve. Le but de cette fois est de dessiner automatiquement ce diagramme de preuve.

Algorithme de recherche de preuves

Taille de la séquence

Avant d'introduire l'algorithme de recherche de preuves, je vais introduire le concept de ** taille ** de la séquence. La taille est le nombre total de symboles logiques $ \ lnot, \ land, \ lor, \ to $ inclus dans la séquence. Par exemple $ A \to B \Rightarrow \lnot A, B $ Puisque la séquence contient $ \ to $ et $ \ lnot $ un par un, la taille est de 2.

Maintenant, regardons à nouveau les règles de raisonnement, en nous concentrant sur la taille. Vous pouvez voir que dans n'importe quelle règle de raisonnement, la taille de la séquence sous la ligne est une plus grande que la taille de la séquence ci-dessus. C'est le point de recherche de preuve.

Séquence de taille 0

Puisque la preuve tire essentiellement des conclusions d'excuses, il est naturel de dessiner des diagrammes de preuve de haut en bas. Cependant, dans la recherche de preuve, lorsqu'une séquence à prouver est donnée, la recherche est effectuée de bas en haut avec celle en bas. Si vous suivez le diagramme de preuve une étape vers le haut, la taille sera réduite de 1, donc quelle que soit la séquence que vous devez prouver, si vous appliquez les règles d'inférence à plusieurs reprises, vous finirez par vous retrouver avec un ensemble de séquences de taille 0. Faire. Une séquence de taille 0 ne peut plus être transformée, vous pouvez donc dire si c'est vrai simplement en regardant s'il s'agit d'une séquence de début.

algorithme

L'algorithme de recherche de preuves est également appelé «algorithme de Wang». C'est un joli nom, mais l'idée est assez naturelle. Il n'y a rien de nouveau. La séquence donnée est réduite à une séquence de taille 0, et si ce sont toutes des séquences de début, la séquence d'origine peut être prouvée, et s'il y en a même une qui n'est pas la séquence de départ, elle ne peut pas être prouvée. J'écrirai en détail ci-dessous. En gros, c'est un algorithme qui détermine si une séquence donnée est une totologie, mais avec un peu d'ingéniosité, vous pouvez également dessiner un diagramme de preuve.

Supposons maintenant que l'on vous donne la séquence $ \ Gamma \ Rightarrow \ Delta $. Tout d'abord, vérifiez si la taille de cette séquence est égale à 0. S'il est égal à 0, vous pouvez déterminer s'il s'agit d'une totologie en déterminant s'il s'agit d'une séquence initiale.

Si la taille est supérieure ou égale à 1, $ \ Gamma \ Rightarrow \ Delta $ contient toujours les symboles logiques $ \ lnot, \ land, \ lor, \ to $. Si vous le recherchez à partir de la gauche et trouvez un symbole logique, vous pouvez suivre les règles d'inférence de bas en haut pour obtenir une ou deux séquences de taille inférieure. De même, déterminez si ces séquences sont de la totologie. La répétition de cette opération aboutira finalement à une séquence de taille 0, et vous pourrez déterminer récursivement si $ \ Gamma \ Rightarrow \ Delta $ est une totologie.

Cela fait longtemps, mais l'idée de base est simple. Nous allons implémenter cet algorithme à partir de maintenant.

Mise en place de la recherche de preuves

Ici, il est implémenté en Python3. Je vais mettre tout le code à la fin de cet article, mais je vais juste écrire la partie importante ici.

Pensez à définir trois classes.

Formule atomique
Formule
Sequent
AtomicFormula Propositions telles que $ P, Q $ qui ne peuvent pas être divisées davantage.

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

N'a qu'un nom. ʻIs_atomic` sera utilisé dans le futur, alors définissez-le.

2. Formule

Il existe diverses expressions logiques telles que $ P \ to Q, \ quad \ lnot (S \ land T), \ quad P \ to ((P \ land Q) \ lor (S \ land T)) $. , En se concentrant sur sa structure hiérarchique, à l'extérieur

\lnot A
A\land B
A\lor B
A\to B Vous pouvez voir qu'il a l'une des formes. Définissez sur cette base.

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 est mis à 1,2,3,4 pour $ \ lnot, \ land, \ lor, \ à $, respectivement. Aussi, définissons ʻis_atomic avec $ A $ comme form1et $ B $ commeform2`.

3. Sequent

La séquence a des colonnes d'expressions logiques à gauche et à droite de $ \ Rightarrow $. La recherche de diagramme de preuve est définie comme une méthode de cette classe.

class Sequent:
    def __init__(self, Left, Right):
        self.Left = Left
        self.Right = Right  #Left,Le droit est la formule,Liste des formules atomiques
    #Lancer le jugement de séquence
    def is_initial(self):
        for l in self.Left:
            if l in self.Right: return True
        return False
    #Jugement séquentiel de taille 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
    #Jugement de thothologie
    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):
        #J'écrirai plus tard

ʻIs_tautology` implémente l'algorithme de Wang et les règles d'inférence telles quelles. Si le premier élément de «Left», «Right» est atomique, il est remplacé par un élément non atomique et la règle d'inférence est appliquée au premier élément.

Vous pouvez maintenant déterminer si cela peut être prouvé en appelant la méthode ʻis_tautology` pour n'importe quelle séquence. Au fait, dans cette définition, par exemple $ A \to B \Rightarrow \lnot A, B $ Est

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

Veuillez noter qu'il est représenté par. Le code qui effectue cette conversion sera reporté.

Passons maintenant à prooftree, la méthode de dessin d'un diagramme de preuve, mais nous utiliserons l'environnement LaTeX prooftree pour écrire le diagramme de preuve. Il est facile à utiliser, vous devriez donc regarder ce site. La méthode prooftree est créée pour renvoyer le code à passer à cet environnement.

Dans cet environnement, écrivez autant que vous pouvez écrire une branche du diagramme de preuve, et si vous ne pouvez pas l'écrire, allez dans une autre branche et intégrez-la. Ce que je veux dire, c'est que j'écris le diagramme de preuve dans l'ordre inverse exact de la recherche de preuve. Ce fait rend très facile la création d'un diagramme de preuve. Il vous suffit d'en ajouter de plus en plus dans le processus d'exploration. Ce qui suit est la définition de «l'arbre de preuve», mais c'est presque la même chose que «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

Enfin, définissez une fonction qui convertit une expression logique (pas une séquence) écrite en utilisant $ \ lnot, \ land, \ lor, \ en $ en classes imbriquées. Puisqu'il est facile de diviser la séquence en expressions logiques, je vais l'omettre. On suppose que $ \ lnot $ a la priorité la plus élevée pour les symboles logiques, et que tout le reste est équivalent. L'implémentation essaie de trouver les symboles logiques de la hiérarchie la plus externe.

def read(exp):
    if '¬' in exp or '∧' in exp or '∨' in exp or '→' in exp:
        #()Trouvez le symbole logique en dehors de
        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)

Cela fait longtemps, mais la mise en œuvre est terminée. À la fin, tout le code est affiché, veuillez donc entrer différentes séquences et essayez-le.

À la fin

Merci d'avoir lu jusqu'ici. Je pense qu'il y avait une partie de l'explication qui était hostile dans le premier article. La description peut être inexacte à certains endroits. Je vous serais reconnaissant si vous pouviez souligner diverses choses. Le code que j'ai écrit cette fois fait moins de 200 lignes au total, donc je pense que vous pouvez voir que vous pouvez facilement créer une preuve automatique en utilisant le calcul de séquence. Bien sûr, il peut être automatisé par d'autres méthodes, il peut donc être intéressant de l'essayer avec des performances naturelles. Ensuite, je mettrai tout le code à la fin.

Tous les 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:
        #()Trouvez le symbole logique en dehors de
        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")