Proof Checker

I worked with Dr. Martin Strauss, Elizabeth Viera, and Dr. Gavin La Rose to build a simple web interface that could be used to automatically check simple proofs as a teaching tool.

A prototype was first built in JavaScript. It has a GitHub repository available here.

A partial implementation for WeBWorK (an open-source online math homework platform) has a GitHub repository here. The development WeBWorK course is here.

Proof Structure

In this project, a proof is a sequence of statements that have justifications.

A statement is some (boolean) expression asserting some fact. Examples of statements include

A justification is the reason it is valid to write a particular statement. Examples include

Proof Verification

A proof is verified by validating a number of things.

Because these checks are all done separately, it's possible to give detailed responses to partially correct / partially complete proofs.

Subproofs

This project uses a system called Natural Deduction. Proofs are sequences of statements and subproofs. Statements are justified given previous in-scope statements.

Subproofs are sequences of statements that begin by supposing some statement is true. Depending on the kind of subproof, different statements may be supposed.

Statements inside a sub-proof are scoped to that subproof (in a way similar to lexical scoping in programming language). The statement is no longer in-scope after the subproof ends, and cannot be referenced by any further justifications.

When a subproof ends, it concludes with a single statement that is in-scope for the remainder of the proof. The conclusion that is allowed depends on the type of subproof that was opened.

For example, this is what a Contradiction subproof looks like.

#StatementJustification
1 ∀x, P(x) ⇒ Q(x) Given
2 ¬Q(5) Given
3 …… P(5) Suppose for Contradiction Subproof
4 …… Q(5) Modus Ponens on 1 and 3
5 ¬P(5) Conclusion of Contradiction Subproof from 2 and 4
6

Notice that statement 3 does not follow from the previous statements. The subproof simply supposes that it is true to derive a contradiction.

Because the subproof concludes in 5, statement 6 may not reference statements 3 or 4.

Notice that statement 4 does depend on statement 3, because it is in the body of the subproof. This is what allows a contradiction to be reached.

The conclusion of the subproof is based on in-scope statements, combined with the statement that was used to introduce the subproof. The statements explicitly listed in the justification are verified to be a contradiction; this fact is used with 3 to produce the conclusion in 6.

Verification Example 1 – Universal Elimination

Justifications are mostly verified by matching the student's statement and the previous statements against different statement structures.

Consider this simple proof involving Universal Elimination

Ex.: Prove that Q(cos(5)+1) is true given that ∀x, Q(x+1) is true.
#StatementJustification
1∀x, Q(x + 1)Given
2Q(cos(5) + 1) Universal Elimination of 1

The justification "Universal Elimination of 1 results 2" needs to be checked.

First, the statements are parsed and turned into trees of operations. (Note that here, there is an explicit function/predicate application operator $)

Statement 1
    1. x
    2. $
      1. Q
      2. +
        1. x
        2. 1
Statement 2
  1. $
    1. Q
    2. +
      1. $
        1. cos
        2. 5
      2. 1

The checker for Universal Elimination begins by matching Statement 1 against a small tree to verify that it is a for-all statement.

    1. variable
    2. predicate

When this match succeeds, we get the assignments

Next, we want to make a pattern from this to check the student's input in Statement 2. To do this, all instances of variable (in this case, just x) are substituted with a pattern-matching-variable instance inside the predicate tree.

This yields the pattern

  1. $
    1. Q
    2. +
      1. instance
      2. 1

The students answer 2 is matched against this pattern, yielding the assignment

Thus, the justification was valid and the statement is justified.

Verification Example 2 – Universal Elimination

Consider the following incorrect proof.

#StatementJustification
1∀x, R(x+1, x+1)Given
2R(6+1, 5+1) Universal Elimination of 1

As in Example 1, first Statement 1 is verified to be a for-all statement. The following pattern is constructed to be used to match valid instantiations of it (by substituting all appearances of variable with a pattern-matching variable instance)

  1. $
    1. R
    2. +
      1. instance
      2. 1
    3. +
      1. instance
      2. 1

This is matched against Statement 2.

It establishes the following assignments:

  1. instance is 6
  2. instance is 5

Note that the same pattern-matching variable is assigned a value twice. Since 5 ≠ 6, the match fails, and the proof checker reports "Not a valid instantiation of ∀x, R(x+1, x+1)"


Consider a similar, correct proof:

#StatementJustification
1∀x, R(x, x)Given
2R(2+3, 3+2) Universal Elimination of 1

This time, the following assignments occur:

  1. instance is 2+3
  2. instance is 3+2

Here, when the second assignment is found, it is compared against the first one. This comparison can be "smart" and know about the commutativity of '+', and thus allow the assignment.

If an instructor wants to disallow these kinds of 'skipping steps', the comparison can be left "dumb" and reject the different form.

Verification Example 3 – Existential Elimination

Here is an example proof that uses the Existential Elimination subproof.

#StatementJustification
1∀x, P(x) ⇒ Q(x) Given
2∃y, P(y)Given
3……P(c)Suppose (for an object called c) from Existential Elimination on 2
4……P(c) ⇒ Q(c) Universal Elimination of 1
5……Q(c) Modus Ponens on 3 and 4
6……∃y, Q(y) Existential Introduction from 5
7∃y, Q(y) Conclusion of Existential Elimination subproof from 6

Note that the kind of statement that can be supposed in a Existential Elimination subproof is fairly limited; the name of a constant is simply given to a there-exists statement.

The conclusion can be any statement that does not involve the name introduced at the beginning.