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

Item Actions

Export

You can export this page using these formats

About

• Item ORO ID
• 12141
• Item Type
• Conference or Workshop Item
• Extra Information
• The software described in this paper is available here.
• Academic Unit or School
• Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
  Faculty of Science, Technology, Engineering and Mathematics (STEM)
• Research Group
• Centre for Research in Computing (CRC)
• Related URLs
• • http://mcs.open.ac.uk/pp2464/alligator/(Other)
• Depositing User
• Paul Piwek