On the Power of Substitution in the Calculus of Structures - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Journal Articles ACM Transactions on Computational Logic Year : 2015

On the Power of Substitution in the Calculus of Structures

Abstract

In this paper we give a direct and simple proof of the known fact that Frege systems with substitution can be p-simulated by the calculus of structures extended with the substitution rule. This is done without referring to extended Frege systems. In the second part of the paper, we then show that the cut-free calculus of structures with substitution is p-equivalent to the cut-free calculus of structures with extension.

Dates and versions

hal-00925707 , version 1 (08-01-2014)

Identifiers

Cite

Lutz Strassburger, Novak Novakovic. On the Power of Substitution in the Calculus of Structures. ACM Transactions on Computational Logic, 2015, 16 (3), ⟨10.1145/2701424⟩. ⟨hal-00925707⟩
223 View
0 Download

Altmetric

Share

Gmail Facebook X LinkedIn More