prover

    This is an attempt at implementing part of Dowek's complete proof search algorithm for the Calculus of Constructions [3].
    To use it, type a term into the lower text field, and press the "try to prove" button.
    Warning: this uses a lot of CPU time (although it does use depth-first search, so memory usage shouldn't be too bad.) Therefore, I wouldn't recommend setting "search depth" higher than 24, or "maximum number of goals to allow" higher than 2.

some examples which work

The applet starts up with pretty much the most trivial goal imaginable (this can be proved using a "search depth" of 4, and a "maximum number of goals"of 2):
!t:#. !x:t. t

modus ponens (provable with a "search depth" of 8, and a "maximum number of goals" of 2)
!a:#. !b:#.
!proofOfA:a. !aImpliesB: (a -> b).
b

"(a and b) implies a" (provable with a "search depth" of 12, and a "maximum number of goals" of 2)
!a: # .
!b: # .
!a_and_b: (!t: # . (a -> (b -> t)) -> t).
a

a first-order example, the first example from Dowek's paper (provable with a "search depth" of 21, and a "maximum number of goals" of 2.) (I modified this slightly, so that the variables to be bound didn't occur in the same order as in the context.)
!T: # .
!R: (T -> (T -> #)) .
!Eq: (T -> (T -> #)) .
!Antisym: !x:T. !y:T. ((R x y) -> ((R y x) -> (Eq x y))) .
!a: T .
!b: T .
!v: R b a .
!u: R a b .
Eq a b

alt="Your browser isn't running the applet, for some reason." Your browser is ignoring the <APPLET> tag!

differences from [3]

To prove a goal ?h:P, using an assumption of type !y_1:Q_1...!y_n:Q_n. Q, the algorithm in [3] creates the subgoals
?h_1:Q_1
.
.
?h_n: Q_n
Q[y_1:=Q_1 . . . y_n:=Q_n] = P

    This algorithm replaces this final equality constraint with a constraint of the form
?h : !Q[y_1:=Q_1 . . . y_n:=Q_n]. P
    This means there don't have to be any equality constraints in the search context.
    This algorithm doesn't implement splitting, and what Dowek calls "product substitutions" don't seem to work either, so this seems limited to first-order proofs.

bugs

    Variable names may clash in the printed representations. (Although the variable "names" used internally are Java object references, and so shouldn't clash.)
    The "splitting" rule and "product substitution" rule, are unimplemented, so this is limited to first-order proofs.
    No attempt is made to inhabit records (Sigma types.)
    This probably should use iterative deepening, instead of having to specify the proof depth in advance.

references

[1] Coquand, T., Huet, G. The calculus of constructions. Information and Computation, Vol. 76, No. 3/4 (1988), pp. 95-120.

[2] Dowek, G., Felty, A., Herbelin, H., Huet, G., Paulin-Mohring, P., Werner, B. The Coq Proof Assistant User's Guide, INRIA-Rochuencourt, CNRS-ENS Lyon, 1991.

[3] Dowek, G. A complete proof synthesis method for the cube of type systems. Journal of Logic and Computation, 3(3):287-315, June 1993.

[4] Strecker, M. Construction and Deduction in Type Theories. Ph.D. thesis. Universitat Ulm, 1999.

[5] Zwanenburg, J. Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow. Ph.D. thesis. Eindhoven University of Technology, 1999.

Josh Burdick / jburdick@gradient.cis.upenn.edu / last modified 20010516