Atomic Metadeduction

Serge Autexier; Dominik Dietrich

In: Bärbel Mertsching (Hrsg.). Proceedings 32nd Annual German Conference on Artificial Intelligence. German Conference on Artificial Intelligence (KI-09), 32nd, September 15-18, Paderborn, Germany, Lectures Notes in Computer Science (LNCS), Springer, 9/2009.


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.


paper.pdf (pdf, 141 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence