TY - BOOK

T1 - Mollusc a general proof-development shell for sequent-based logics

AU - Richards, Bradley L

AU - Kraan, Ina

AU - Smaill, Alan

AU - Wiggins, Geraint A

PY - 1994

Y1 - 1994

N2 - This article describes an interactive proof development shell, Mollusc [Richards 93], 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-Löf 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 proofplanner interface, and provides for automated proof construction through a tactic language and interpreter.

AB - This article describes an interactive proof development shell, Mollusc [Richards 93], 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-Löf 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 proofplanner interface, and provides for automated proof construction through a tactic language and interpreter.

M3 - Book

BT - Mollusc a general proof-development shell for sequent-based logics

PB - Springer-Verlag

ER -