provers.py

""" (c) This file is part of the course
    Mathematical Logic through Programming
    by Gonczarowski and Nisan.
    File name: code/propositions/provers.py """

from functools import lru_cache

from propositions.syntax import *
from propositions.proofs import *

# Tautological Inference Rules
MP = InferenceRule([Formula.from_infix('p'), Formula.from_infix('(p->q)')],
                   Formula.from_infix('q'))

I1 = InferenceRule([], Formula.from_infix('(p->(q->p))'))
I2 = InferenceRule([], Formula.from_infix('((p->(q->r))->((p->q)->(p->r)))'))

N  = InferenceRule([], Formula.from_infix('((~p->~q)->(q->p))'))

A1 = InferenceRule([], Formula.from_infix('(p->(q->(p&q)))'))
A2 = InferenceRule([], Formula.from_infix('((p&q)->p)'))
A3 = InferenceRule([], Formula.from_infix('((p&q)->q)'))

O1 = InferenceRule([], Formula.from_infix('(p->(p|q))'))
O2 = InferenceRule([], Formula.from_infix('(q->(p|q))'))
O3 = InferenceRule([], Formula.from_infix('((p->r)->((q->r)->((p|q)->r)))'))

T  = InferenceRule([], Formula.from_infix('T'))

F  = InferenceRule([], Formula.from_infix('~F'))

AXIOMATIC_SYSTEM = [MP, I1, I2, N, A1, A2, A3, O1, O2, O3, T, F]

@lru_cache(maxsize=1) # Cache the return value of prove_implies_self
def prove_implies_self():
    """ Return a valid deductive proof for '(p->p)' via MP,I1,I2 """
    # Task 5.1
    # Indices: MP: 0, I1: 1, I2: 2
    l1 = DeductiveProof.Line(Formula.from_infix(
        '(p->((p->p)->p))'), 1, [])
    l2 = DeductiveProof.Line(Formula.from_infix(
        '((p->((p->p)->p))->((p->(p->p))->(p->p)))'), 2, [])
    l3 = DeductiveProof.Line(Formula.from_infix(
        '((p->(p->p))->(p->p))'), 0, [0,1])
    l4 = DeductiveProof.Line(Formula.from_infix(
        '(p->(p->p))'), 1, [])
    l5 = DeductiveProof.Line(Formula.from_infix(
        '(p->p)'), 0, [3,2])
    lines = [l1, l2, l3, l4, l5]
    return DeductiveProof(InferenceRule(
        [], Formula.from_infix('(p->p)')), [MP, I1, I2], lines)


def _different_assumption_lines(line, assumption, line_num):
    """Create appropriate lines for assumption/no assumptions line"""
    l1 = line
    l2 = DeductiveProof.Line((Formula('->', line.conclusion, Formula('->', assumption, line.conclusion))), 1, [])
    l3 = DeductiveProof.Line(Formula('->', assumption, line.conclusion), 0, [line_num, 1 + line_num])
    return [l1, l2, l3]


def _find_justification_line(new_lines, justification):
    """finds the correct line number for the justification"""
    for i, line in enumerate(new_lines):
        if line.conclusion == justification:
            return i
    return None

def _MP_lines(assumption, new_lines, f7, f13):
    """Create appropriate lines for a MP line"""
    l1_formula = instantiate(I2.conclusion, {
        'p' : assumption,
        'r' : f13,
        'q' : f7
    })
    part1 = l1_formula.first
    part2 = l1_formula.second
    part1_justif = _find_justification_line(new_lines, part1)
    a_f7_jusif = _find_justification_line(new_lines, part2.first) # a->f7 justif
    assert part1_justif is not None and a_f7_jusif is not None
    l1 = DeductiveProof.Line(l1_formula, 2, [])
    l2 = DeductiveProof.Line(part2, 0, [part1_justif, len(new_lines)])
    l3 = DeductiveProof.Line(part2.second, 0, [a_f7_jusif, len(new_lines) + 1])
    return [l1, l2, l3]



def inverse_mp(proof, assumption):
    """ Return a valid deductive proof for '(assumption->conclusion)', where
        conclusion is the conclusion of proof, from the assumptions of proof
        except assumption, via MP,I1,I2 """
    # Task 5.3


    new_assumptions = [assump for assump in proof.statement.assumptions if assump != assumption]
    new_statement = InferenceRule(new_assumptions, Formula('->', assumption, proof.statement.conclusion))
    rules_without_as = [i for i, rule in enumerate(proof.rules) if not rule.assumptions] # rule has no assump
    new_lines = []
    new_proof = DeductiveProof(new_statement, proof.rules, new_lines)

    ################## proving the assumption at the beginning #################
    self_proof = prove_implies_self()
    assump_proof = prove_instance(self_proof, InferenceRule([], Formula('->', assumption, assumption)))
    new_lines += assump_proof.lines

    ################## handling every line ##################
    # we need to replace every line with
    # assumption_to_remove -> line.conclusion
    # There are four cases.
    line_num = 5 # implies self length is 5
    for line in proof.lines:
        # if line is the assumption we need to remove
        if line.conclusion == assumption:
            # already implemented before the loop
            continue
        elif not line.justification:  # line is an assumption
            new_lines += _different_assumption_lines(line, assumption, line_num)
            line_num += 3
        elif line.rule in rules_without_as: # rules in rules no assumptions
            new_lines += _different_assumption_lines(line, assumption, line_num)
            line_num += 3
        else: # line has rule with assumption
            f7 = proof.lines[line.justification[0]].conclusion
            f13 = proof.lines[line.justification[1]].conclusion.second
            new_lines += _MP_lines(assumption, new_lines, f7, f13)
            line_num += 3
    #####################################
    return new_proof

@lru_cache(maxsize=1) # Cache the return value of prove_hypothetical_syllogism
def prove_hypothetical_syllogism():
    """ Return a valid deductive proof for '(p->r)' from the assumptions
        '(p->q)' and '(q->r)' via MP,I1,I2 """
    # Task 5.4
    p = Formula.from_infix('p')
    assumptions = [Formula.from_infix('(p->q)'), Formula.from_infix('(q->r)'), p]
    conclusion = Formula.from_infix('r')
    l1 = DeductiveProof.Line(assumptions[0])
    l2 = DeductiveProof.Line(assumptions[1])
    l3 = DeductiveProof.Line(p)
    l4 = DeductiveProof.Line(Formula.from_infix('q'), 0, [2,0])
    l5 = DeductiveProof.Line(Formula.from_infix('r'), 0, [3,1])
    lines = [l1, l2, l3, l4, l5]
    semi_p = DeductiveProof(InferenceRule(assumptions, conclusion), [MP, I1, I2], lines)
    assert semi_p.is_valid()
    return inverse_mp(semi_p, p)