Publication
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.
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.