The ALLIGATOR Theorem Prover for Dependent Type Systems: Description and Proof Sample.
In: Proceedings of the 5th Workshop on Inference in Computational Semantics (ICoS-5), 20 - 21 April 2006, Buxton, UK.
Full text available as:
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.
Actions (login may be required)