From deep inference to proof nets via cut elimination
L Straßburger - Journal of Logic and Computation, 2009 - academic.oup.com
Journal of Logic and Computation, 2009•academic.oup.com
This article shows how derivations in the deep inference system SKS for classical
propositional logic can be translated into proof nets. Since an SKS derivation contains more
information about a proof than the corresponding proof net, we observe a loss of information
which can be understood as 'eliminating bureaucracy'. Technically, this is achieved by cut
reduction on proof nets. As an intermediate step between the two extremes, SKS derivations
and proof nets, we will see proof graphs representing derivations in 'Formalism A'.
propositional logic can be translated into proof nets. Since an SKS derivation contains more
information about a proof than the corresponding proof net, we observe a loss of information
which can be understood as 'eliminating bureaucracy'. Technically, this is achieved by cut
reduction on proof nets. As an intermediate step between the two extremes, SKS derivations
and proof nets, we will see proof graphs representing derivations in 'Formalism A'.
Abstract
This article shows how derivations in the deep inference system SKS for classical propositional logic can be translated into proof nets. Since an SKS derivation contains more information about a proof than the corresponding proof net, we observe a loss of information which can be understood as ‘eliminating bureaucracy’. Technically, this is achieved by cut reduction on proof nets. As an intermediate step between the two extremes, SKS derivations and proof nets, we will see proof graphs representing derivations in ‘Formalism A’.
Oxford University Press顯示最佳搜尋結果。 查看所有結果