| Autor: |
Hutchison, David, Kanade, Takeo, Kittler, Josef, Kleinberg, Jon M., Mattern, Friedemann, Mitchell, John C., Naor, Moni, Nierstrasz, Oscar, Pandu Rangan, C., Steffen, Bernhard, Sudan, Madhu, Terzopoulos, Demetri, Tygar, Doug, Vardi, Moshe Y., Weikum, Gerhard, Comon-Lundh, Hubert, Kirchner, Claude, Kirchner, Hélène, Brauner, Paul, Houtmann, Clément |
| Zdroj: |
Rewriting, Computation & Proof; 2007, p132-166, 35p |
| Abstrakt: |
Superdeduction is a systematic way to extend a deduction system like the sequent calculus by new deduction rules computed from the user theory. We show how this could be done in a systematic, correct and complete way. We prove in detail the strong normalisation of a proof term language that models appropriately superdeduction. We finally examplify on several examples, including equality and noetherian induction, the usefulness of this approach which is implemented in the $\sf{lemurid{\ae}}$ system, written in TOM. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
