ALLIGATOR: A Natural Deduction Theorem Prover with proofs as typed lambda terms

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.