Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >
-->

small logo

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.

 

System

Higher Order Unification

Accumulates Conclusions

Proof Search

Can vary rules and strategies

PVS

Matching

No

Some

Yes

HOL-Light

Yes

No

MESON_TAC

No

Isabelle

Yes

No

No

Yes

NuPrl

No

No

No

No

Coq

Yes

No

No

No

Theorema

No

No

Some

Yes

λ-Prolog

Yes

No

HH formulas only

No

TPS

Yes

Yes

Yes

Some

ACL2

No

No

Yes

No

Otter

No

Yes

Yes

Yes

Otter-λ

Some

Yes

Yes

Yes