| Publication type: |
Article in Proceedings |
| Author: |
Serge Autexier; Dominik Dietrich |
| Editor: |
Bärbel Mertsching |
| Title: |
Atomic Metadeduction |
| Book / Collection title: |
Proceedings 32nd Annual German Conference on Artificial Intelligence. 32nd Annual German Conference on Artificial Intelligence (KI-09), September 15-18, Paderborn, Germany, Germany |
| Series: |
Lecture Notes in Artificial Intelligence |
| Year published: |
2009 |
| Publisher: |
Springer-Verlag Berlin Heidelberg |
| Abstract: |
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 |
| Last updated: |
14. 10. 2009 |
