Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive ...

Superdeduction and deduction modulo are two methods designed to ease the use of first-order theories in predicate logic. Superdeduction modulo combines both in a single framework. Although soundness is ensured, using superdeduction modulo to extend ...

Superdeduction is a formalism closely related to deduction modulo which permits to enrich a deduction system (especially a first-order one such as natural deduction or sequent calculus) with new inference rules automatically computed from the ...

Deduction Modulo implements Poincarés principle by identifying deduction and computation as different paradigms and making their interaction possible. This leads to logical systems like the sequent calculus or natural deduction modulo. Even if deduction ...

Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen's intuitionistic sequent calculus LJ, that relies on completeness of the cut-free calculus with respect to Kripke Models. The ...

Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...