I tried to implement automatic proof of sequence calculation

This article was written as the 21st day of ISer Advent Calendar 2019.

Introduction

In this article, we will implement an automated proof using sequent calculus of classical propositional logic called G3C. However, I will focus on the implementation without going too far into the rigorous theory. What you make in this article is, for example, $ \lnot P \lor Q \Rightarrow P \to Q If you give the sequence of $ as input It will output a proof diagram like this. There are several proof systems other than sequent calculus, but sequent calculus is known to make such automatic proofs easy. Therefore, I will try to implement this this time.

What is sequent calculus?

Sequent

Sequent is simply a proposition. For example $ A,B \Rightarrow C,D $ The sequence represents the proposition "If A and B are ** both ** true, then ** at least one of C and D is ** true". When this proposition is correct, we will say that this sequence is ** tautology **.

For example, the following sequence can be said to be a tautology. $ A \to B \Rightarrow \lnot A, B $ If "B if A" is true, then "not A" or "is B" holds. The reason why it holds is that it can be proved using the proof system of sequent calculus. Many people think that this proposition is intuitively correct, but the proof system for sequent calculus is designed not to go against such intuition.

Logical symbol

In the previous proposition, $ \ lnot $ and $ \ to $ came out as logical symbols. There are only four types of logical symbols in propositional logic. They are in line with the intuitive meaning.

symbol	Example	meaning
\lnot	\lnot A	Not A
\land	A\land B	A and B
\lor	A\lor B	A or B
\to	A \to B	If A, then B

Inference rules

You must be able to infer to make a proof. Inference is expressed in the following form. $ \cfrac{A \Rightarrow B}{C \Rightarrow D} $ This means that if the sequence $ A \ Rightarrow B $ is a tautology, then the sequence $ C \ Rightarrow D $ is also a tautology, that is, $ C \ Rightarrow D $ can be derived from $ A \ Rightarrow B $.

The following eight types of inference rules are defined in the G3C proof system. The proof will be constructed using these eight types of inference rules. In addition, the order of logical expressions shall be arbitrarily changed on each side of the sequence. $ \ 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 left) \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} (\ to left) \qquad \ cfrac {A, \ Gamma \ Rightarrow \ Delta, B} {\ Gamma \ Rightarrow \ Delta, A \ to B} (\ to right) $ These inference rules are intuitively convincing. Take, for example, the inference of "$ \ lnot $ left". Now, assuming $ \ Gamma $, we know that $ \ Delta $ or $ A $ holds.

(i) If $ \ Delta $ can be derived from $ \ Gamma $, then of course $ \ lnot A, \ Gamma \ Rightarrow \ Delta $ is tautological. (ii) If $ A $ can be derived from $ \ Gamma $, then $ \ lnot A and \ Gamma $ will never be true, so $ \ lnot A, \ Gamma \ Rightarrow \ Delta $ is tautological regardless of the right side. It's true.

I won't write about other inference rules, but I think you can be convinced by thinking this way.

Start sequence

Now, we will prove by combining the above inference rules, but for that purpose we need a sequence that is an axiom located at the top of the proof diagram. This is called the ** start sequence **. This should be a sequence that is self-evidently true to everyone. The sequence that can be derived from the tautological sequence is also tautological.

The starting sequence in the proof system dealt with here is only the one in the following form. $ P,\Gamma \Rightarrow P,\Delta $ If $ P, \ Gamma $ are both true, then at least one of $ P, \ Delta $ is true. It's natural because $ P $ is true.

Proof

Given a sequence to prove, if the inference rule is repeatedly applied from the start sequence and the final sequence is matched, the proof is complete.

As an example, the first sequence I gave $ A \to B \Rightarrow \lnot A, B $ Let's prove according to this rule. The following is the proof. The goal of this time is to draw this proof diagram automatically.

Proof search algorithm

Sequent size

Before introducing the proof search algorithm, let us introduce the concept of the ** size ** of the sequence. The size is the total number of logical symbols $ \ lnot, \ land, \ lor, \ to $ included in the sequence. For example $ A \to B \Rightarrow \lnot A, B $ Since the sequence contains $ \ to $ and $ \ lnot $ one by one, the size is 2.

Now, let's look at the inference rules again, focusing on size. You can see that in any inference rule the size of the sequence below the line is one larger than the size of the sequence above. This is the point of proof search.

Sequent of size 0

Since proof basically draws conclusions from axioms, it is natural to draw a proof diagram from top to bottom. However, in the proof search, when a sequence to be proved is given, the search is performed from bottom to top with that as the bottom. If you follow the proof diagram one step up, the size will be reduced by 1, so no matter what sequence you have to prove, if you apply the inference rule repeatedly, you will eventually end up with a set of sequences of size 0. To do. A zero-sized sequence can't be transformed anymore, so you can tell if it's taut by just looking at whether it's a start sequence.

algorithm

The proof search algorithm is also called the "Wang algorithm". It's a nice name, but the idea is quite natural. There is nothing new. The given sequence is reduced to a sequence of size 0, and if they are all start sequences, the original sequence can be proved, and if any one is not the start sequence, it cannot be proved. I will write in detail below. Basically, it is an algorithm that determines whether a given sequence is tautology, but with a little ingenuity, you can also draw a proof diagram.

Now suppose you are given the sequence $ \ Gamma \ Rightarrow \ Delta $. First, check if the size of this sequence is 0. If it is 0, it can be determined whether it is a tautology by determining whether it is an initial sequence.

If the size is greater than or equal to 1, $ \ Gamma \ Rightarrow \ Delta $ always contains the logical symbols $ \ lnot, \ land, \ lor, \ to $. If you search it from the left and find a logical symbol, you can follow the inference rules from bottom to top to get one or two sequences that are one smaller in size. Similarly, determine if those sequences are tautologies. Repeating this operation will eventually result in a sequence of size 0, and you can recursively determine if $ \ Gamma \ Rightarrow \ Delta $ is a tautology.

It's been a long time, but the basic idea is simple. We will implement this algorithm from now on.

Implementation of proof search

Here, it is implemented in Python3. I'll put the whole code at the end of this article, but I'll write only the important parts here.

Consider defining three classes.

Atomic Formula
Formula
Sequent
AtomicFormula Propositions such as $ P, Q $ that cannot be further divided.

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

Has only a name. ʻIs_atomic` will be used in the future, so define it.

2. Formula

There are various logical expressions such as $ P \ to Q, \ quad \ lnot (S \ land T), \ quad P \ to ((P \ land Q) \ lor (S \ land T)) $. , Focusing on its hierarchical structure, on the outermost side

\lnot A
A\land B
A\lor B
A\to B You can see that it has one of the forms. Define based on this.

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

We will define self.relation as 1,2,3,4 for $ \ lnot, \ land, \ lor, \ to $, respectively. Also, let's define ʻis_atomic with $ A $ as form1and $ B $ asform2`.

3. Sequent

The sequence has columns of formulas to the left and right of $ \ Rightarrow $. The proof diagram search is defined as a method of this class.

class Sequent:
    def __init__(self, Left, Right):
        self.Left = Left
        self.Right = Right  #Left,Right is Formula,List of Atomic Formula
    #Start sequence judgment
    def is_initial(self):
        for l in self.Left:
            if l in self.Right: return True
        return False
    #Sequent judgment of size 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
    #Tautology judgment
    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):
        #I will write later

ʻIs_tautologyimplements Wang's algorithm and inference rules as they are. If the first element ofLeft, Right` is atomic, it is replaced with a non-atomic element, and the inference rule is applied to the first element.

Now you can determine if it can be proved by calling the ʻis_tautology` method for any sequence. By the way, in this definition, for example $ A \to B \Rightarrow \lnot A, B $ Is

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

Please note that it is represented as. The code that does this conversion will be postponed.

Now let's get down to prooftree, the method of drawing a proof diagram, but we'll use LaTeX's prooftree environment to write the proof diagram. It's easy to use, so you should look at this site. The prooftree method is created to return the code to pass to this environment.

In this environment, write as much as you can write one branch of the proof diagram, and if you can not write it, go to another branch and integrate it. What I want to say is that I write the proof diagram in the exact reverse order of the proof search. This fact makes it very easy to draw a proof diagram. You just have to add more and more in the process of exploration. The following is the definition of proof tree, which is almost the same as ʻ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

Finally, define a function that converts a logical expression (not a sequence) written using $ \ lnot, \ land, \ lor, \ to $ into nested classes. It is easy to divide the sequence into logical expressions, so I will omit it. It is assumed that $ \ lnot $ has the highest priority for logical symbols, and that everything else is equivalent. The implementation is trying to find the logical symbols of the outermost hierarchy somehow.

def read(exp):
    if '¬' in exp or '∧' in exp or '∨' in exp or '→' in exp:
        #()Find the logical symbol outside of
        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)

It's been a long time, but the implementation is over. The whole code is posted at the end, so please enter various sequences and try it out.

At the end

Thank you for reading this far. I think there was a part of the explanation that was unfriendly in the first article. The description may be inaccurate in some places. I would appreciate it if you could point out various things. The code I wrote this time is less than 200 lines in total, so I think you can see that you can easily create an automated proof by using sequent calculus. Of course, it can be automated by other methods, so it may be interesting to try natural deduction. Then, I will put all the codes at the end.

All chords

# -*- 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:
        #()Find the logical symbol outside of
        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")