Name
Abstract | ||
|---|---|---|
This article describes an interactive proof development shell, Mollusc[Richards 93], which can be used to construct and edit proofs in sequentbasedlogics. Conceptually, Mollusc may be thought of as a logic-independentsuccessor to Oyster [Bundy et al 90]. However, where Oyster wastied to a variant of Martin-Lof type theory, Mollusc can be used with anysequent-based logic for which a suitable definition is provided. Althoughdeveloped in a research environment, Mollusc should also be... |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/3-540-58156-1_69 | CADE |
Keywords | Field | DocType |
general proof-development shell,sequent-based logics,martin lof type theory | Discrete mathematics,Computer science,Successor cardinal,Type theory,Algorithm,Mathematical proof,Interpreter,Sequent,Rule of inference | Conference |
ISBN | Citations | PageRank |
3-540-58156-1 | 2 | 0.59 |
References | Authors | |
5 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bradley L. Richards | 1 | 209 | 37.47 |
| Ina Kraan | 2 | 183 | 18.79 |
| Alan Smaill | 3 | 854 | 86.81 |
| Geraint Wiggins | 4 | 401 | 52.80 |