The Open UniversitySkip to content

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 April 2006, Buxton, UK.

Full text available as:
PDF (Not Set) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (1167Kb)
Google Scholar: Look up in Google Scholar


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.

Item Type: Conference Item
Extra Information: The software described in this paper is available here.
Academic Unit/Department: Mathematics, Computing and Technology > Computing & Communications
Mathematics, Computing and Technology
Interdisciplinary Research Centre: Centre for Research in Computing (CRC)
Related URLs:
Item ID: 12141
Depositing User: Paul Piwek
Date Deposited: 29 Oct 2008 02:42
Last Modified: 24 Feb 2016 06:20
Share this page:

Download history for this item

These details should be considered as only a guide to the number of downloads performed manually. Algorithmic methods have been applied in an attempt to remove automated downloads from the displayed statistics but no guarantee can be made as to the accuracy of the figures.

▼ Automated document suggestions from open access sources

Actions (login may be required)

Policies | Disclaimer

© The Open University   + 44 (0)870 333 4340