Proof by Contradiction

Geoff Sutcliffe
University of Miami
geoff[@]cs.miami.edu

Introduction

Most proofs output from modern ATP systems are proofs by contradiction of the clause normal form of the axioms and negated conjecture. For example:

fof(a,axiom,
    a ).

fof(a_implies_b,axiom,
    a => b ).

fof(b,conjecture,
    b ).

fof(f1,negated_conjecture,
    ~b,
     inference(negate,[status(cth)],[b]) ).

cnf(c1,plain,
    a,
    inference(cnf,[status(thm)],[a]) ).

cnf(c2,plain,
    ~a | b,
    inference(cnf,[status(thm)],[a_implies_b]) ).

cnf(c3,plain,
    ~b,
    inference(cnf,[status(thm)],[f1]) ).

cnf(c4,plain,
    ~a,
    inference(resolution,[status(thm)],[c2,c3]) ).

cnf(c5,plain,
    $false,
    inference(resolution,[status(thm)],[c1,c4]) ).

The weakness of this form is that the theorem is not at the root, which means it is not possible to graft derivations together, with the proved root theorem of one being used as a lemma of the next.

A Better Way

A better way might be to do something similar to what is done in ND. The negated conjecture is introduced as an assumption, recorded as an assumption in all of its descendent formulae, and must be discharged by being added as the antecedent of an implication with the current formula as consequent. For example:

fof(a,axiom,
    a ).

fof(a_implies_b,axiom,
    a => b ).

fof(b,conjecture,
    b ).

fof(f1,assumption,
    ~b,
    introduced(assumption,[negate(b)]) ).

cnf(c1,plain,
    a,
    inference(cnf,[status(thm)],[a]) ).

cnf(c2,plain,
    ~a | b,
    inference(cnf,[status(thm)],[a_implies_b]) ).

cnf(c3,plain,
    ~b,
    inference(cnf,[status(thm),assumptions([f1])],[f1]) ).

cnf(c4,plain,
    ~a,
    inference(resolution,[status(thm),assumptions([f1])],[c2,c3]) ).

cnf(c5,plain,
    $false,
    inference(resolution,[status(thm),assumptions([f1])],[c1,c4]) ).

fof(f2,plain,
    ~b => $false,
    inference(discharge,[status(thm)],assumptions([])],[c5,f1]) ).

fof(f3,theorem,
    b,
    inference(simplify,[status(thm)],assumptions([])],[f2]) ).

This can also be used for recording explicit splits, as done by SPASS:

fof(a,axiom,
    a ).

fof(a_implies_b,axiom,
    a => b ).

fof(b,conjecture,
    b ).

fof(f1,assumption,
    ~b,
    introduced(assumption,[negate(b)]) ).

cnf(c1,plain,
    a,
    inference(cnf,[status(thm)],[a]) ).

cnf(c2,plain,
    ~a | b,
    inference(cnf,[status(thm)],[a_implies_b]) ).

cnf(c3,plain,
    ~b,
    inference(cnf,[status(thm),assumptions([f1])],[f1]) ).

cnf(c4,assumption,
    ~b,
    introduced(assumption,[split(c2)]) ).

cnf(c5,plain,
    ~a,
    inference(resolution,[status(thm),assumptions([c4])],[c2,c4]) ).

cnf(c6,plain,
    $false,
    inference(resolution,[status(thm),assumptions([c4])],[c1,c5]) ).

fof(f2,plain,
    ~b => $false,
    inference(discharge,[status(thm),assumptions([])],[c6,c4]) ).

fof(f3,plain,
    b,
    inference(simplify,[status(thm),assumptions([])],[f2]) ).

cnf(c7,plain,
    b,
    inference(cnf,[status(thm),assumptions([])],[f3]) ).

cnf(c8,plain,
    $false,
    inference(resolution,[status(thm),assumptions([f1])],[c3,c7]) ).

fof(f4,plain,
    ~b => $false,
    inference(discharge,[status(thm),assumptions([])],[c8,f1]) ).

fof(f5,theorem,
    b,
    inference(simplify,[status(thm),assumptions([])],[f4]) ).