| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Serge Autexier; Dominik Dietrich |
| Herausgeber: |
Bärbel Mertsching |
| Titel: |
Atomic Metadeduction |
| Buch / Sammlungs-Titel: |
Proceedings 32nd Annual German Conference on Artificial Intelligence. 32nd Annual German Conference on Artificial Intelligence (KI-09), September 15-18, Paderborn, Germany, Germany |
| Serie / Reihe: |
Lecture Notes in Artificial Intelligence |
| Erscheinungsjahr: |
2009 |
| Verleger: |
Springer-Verlag Berlin Heidelberg |
| Abstract / Kurzbeschreibung: |
We present an extension of the first-order logic sequent calculus SK that allows us to systematically add inference rules derived from arbitrary axioms, definitions, theorems, as well as local hypotheses -- collectively called assertions. Each derived deduction rule represents a pattern of larger SK-derivations corresponding to the use of that assertion. The idea of metadeduction is to get shorter and more concise formal proofs by allowing the replacement of any assertion in the antecedent of a sequent by derived deduction rules that are available locally for proving that sequent. We prove the soundness and completeness for atomic metadeduction, which builds upon a permutability property for the underlying sequent calculus SK with liberalized $deltaplusplus$-rule. |
| Internet: |
https://www2.dfki.de/intranet/research/publications/renameFileForDownload?filename=paper.pdf&file_id=uploads_336 |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
14. 10. 2009 |
