ALLIGATOR is a theorem prover for Dependent Type Systems (DTS; see item 4 below for an introduction to DTS). 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. The main advantage of using Dependent Type Systems for theorem proving is that the prover not only tells you whether or not it can prove a certain proposition given a set of assumptions, but also returns a formal representation of the (natural deduction) proof, if it can find one (this proof-object is a term of the typed lambda calculus).
Documentation
Piwek, P. (2006). ALLIGATOR 1.0 Manual. March 2006. [.txt]
Piwek, P. (2006). The ALLIGATOR Theorem Prover for Dependent Type Systems: Description and Proof Sample. In: Proceedings of Workshop on Inference in Computational Semantics (ICoS-5), April 2006, Buxton, UK. (6 pages). This paper introduces the ALLIGATOR theorem prover for Dependent Type Systems (DTS). We start with highlighting a number of properties of DTS that make them specifically suited for computational semantics. We then briefly introduce DTS and our implementation. The paper concludes with an example of a DTS proof that illustrates the suitability of DTS for modelling anaphora resolution. [.pdf] [When referring to the Alligator Theorem Prover, please cite this paper]
Piwek, P. (2006) ALLIGATOR: Theorem Proving for DTS with Sigma Types. Manuscript. March 2006. (14 pages) This paper contains a detailed introduction to and description of the Dependent Type System (Pure Type System with Sigma Types) on which ALLIGATOR is based. [.pdf]
