Brief description

ALLIGATOR is a natural deduction theorem prover which can deal with propositional, predicate and higher order logics. It has been implemented in both Sicstus and the freely available SWI prolog. The source code is available free of charge under a Creative Commons license.

ALLIGATOR is based on Dependent Type Systems. The main advantage of using Dependent Type Systems for theorem proving is that if the prover can infer a certain proposition from given a set of assumptions, it will not only tell you so but also return a representation of the (natural deduction) proof. Exploiting the Curry-Howard-De Bruijn correspondence between logic and type systems, this proof object is a term of the typed lambda calculus.

Documentation

• ALLIGATOR 1.0 Manual. March 2006.
• ALLIGATOR Query Examples. March 2006.
• The ALLIGATOR Theorem Prover for Dependent Type Systems: Description and Proof Sample.
  (ICOS workshop paper, 6 pages)
• ALLIGATOR: Theorem Proving for DTS with Sigma Types.
  (Manuscript with detailed description of the theorem prover, 14 pages)
• Further work on inferentialist semantics and pragmatics which motivated the development of the Alligator theorem prover.