Online Otter-λ

Examples

This example is almost the same as quantifiers5.in. Therefore, you should read the commentary file quantifiers5.html before reading this one. The one difference in the input files is that this file makes use of the user-defined typing facility available in Otter-λ. The "implicit types" in quantifiers5.in are made explicit using list(types) in this example. This forces Otter-λ to respect those typings when lambda-unifications are performed.

The interesting thing is that the proof produced is different. The deduction of i(x,Ap(a,c)), which takes place immediately in quantifiers5, is postponed quite a few steps in quantifiers8, and derived in a different way. We have not yet had time to determine the reason for this; it may turn out to be a bug in the type-enforcement mechanism, which has not yet been thoroughly tested. But both proofs are valid.