Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #723 | |
|---|---|
| Title: | Mollusc a General Proof-Development Shell for Sequent-Based Logics |
| Authors: | Richards,B; Kraan,I; Smaill,AD; Wiggins,A |
| Date: | Dec 1994 |
| Presented: | Appeared in CADE 12, A. Bundy (ed), Springer Lecture Notes in AI vol. 814, 1994, pp 826-30. |
| Keywords: | |
| Abstract: | This article describes an interactive proof development shell, Mollusc [Richards 93]m which can be used to construct and edit proofs in sequent-based logics. Conceptually, Mollusc may be thought of as a logic-independent successor to Oyster [Bundy et al 90]. However, where Oyster was tied to a variant of Martin-Loef type theory, Mollusc can be used with any sequent-based logic for which a suitable definition is provided. Although developed in a research environment, Mollusc should also be suitable for use in classroom exercises. In addition to proof editing facilities, Mollusc supports the definition of new logics, includes a proof-planner interface, and provides for automated proof construction through a tactic language and interpreter. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}