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:

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
Interdisciplinary Research Centre:	Centre for Research in Computing (CRC)
Related URLs:	http://mcs.open.ac.uk/pp2464/alligator/(Other)
Item ID:	12141
Depositing User:	Paul Piwek
Date Deposited:	29 Oct 2008 02:42
Last Modified:	26 Jan 2011 10:35
URI:	http://oro.open.ac.uk/id/eprint/12141

Actions (login may be required)

	View Item
RDF+XMLBibTeXRDF+N-TriplesJSONDublin CoreAtomOAI-ORE Resource Map (Atom Format)Simple MetadataReferMETSOAI-ORE Resource Map (RDF Format)HTML CitationASCII CitationMultiline CSVRefMan RIS Format (UTF-8)OpenURL ContextObjectEndNoteMODSOpenURL ContextObject in SpanMPEG-21 DIDLEP3 XMLRefMan RIS FormatRDF+N3Eprints Application Profile	Public: Report issue / request change