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:
[img]
Preview
PDF (Not Set) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (1167Kb)
URL: http://www.cs.man.ac.uk/~ipratt/ICoS-5/
Google Scholar: Look up in Google Scholar

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.

Item Type: Conference Item
Extra Information: The software described in this paper is available here.
Academic Unit/Department: Mathematics, Computing and Technology > Computing & Communications
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: 25 Nov 2014 08:57
URI: http://oro.open.ac.uk/id/eprint/12141
Share this page:

Actions (login may be required)

View Item
Report issue / request change

Policies | Disclaimer

© The Open University   + 44 (0)870 333 4340   general-enquiries@open.ac.uk