Axiom directed Focusing

Long versionInternational audienceSuperdeduction and deduction modulo are methods specially designed to ease the use of first-order theories in predicate logic. Superdeduction modulo, which combines both, enables the user to make a distinct use of computational and reasoning axioms. Although soundness is ensured, using superdeduction and deduction modulo to extend deduction with awkward theories can jeopardize essential properties of the extended system such as cut-elimination or completeness \wrt~predicate logic. Therefore one has to design criteria for theories which can safely be used through superdeduction and deduction modulo. In this paper we revisit the superdeduction paradigm by comparing it with the focusing approach. In particular we prove a focalization theorem for cut-free superdeduction modulo: we show that permutations of inference rules can transform any cut-free proof in deduction modulo into a cut-free proof in superdeduction modulo and conversely, provided that some hypotheses on the synchrony of reasoning axioms are verified. It implies that cut-elimination for deduction modulo and for superdeduction modulo are equivalent. Since several criteria have already been proposed for theories that do not break cut-elimination of the corresponding deduction modulo system, these criteria also imply cut-elimination of the superdeduction modulo system, provided our synchrony hypotheses hold. Finally we design a tableaux method for superdeduction modulo which is sound and complete provided cut-elimination holds