The ALLIGATOR Theorem Prover for Dependent Type Systems: Description and Proof Sample

Piwek, Paul (2006). 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 Apr 2006, Buxton, UK.

URL: http://www.cs.man.ac.uk/~ipratt/ICoS-5/

Abstract

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.

Viewing alternatives

Look up in Google Scholar

Download history

Item Actions

Export

About

CORE (COnnecting REpositories)