Online Otter-λ

The following table compares key features of several theorem-provers and proof-checking systems. You will note that Otter-λ is the only one without a "no" entry in any column. The first column, labeled Higher Order Unification, refers to the use of higher-order or second-order unification, or in Otter-λ's case, untyped lambda-unification. The entry for Otter-λ is "some" rather than "yes", since Otter-λ at present returns only one unifier, when there may be several; but on the other hand, Otter-λ can succeed in some untyped unifications that fail in typed systems. The second column Accumulates Conclusion refers to the ability to accumulate derived conclusions in a "database" of deduced conclusions, that can be searched for the generation of new conclusions. The column Proof Search refers to the ability to search for a proof (as opposed to checking a proof entered by the user or developed interactively). The last column refers to whether the system can allow the user precise control over the rules of inference to be used, and to specify "strategies" that control the proof search, such as discarding or favoring formulas of certain forms.