Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible to check the correctness of a net (...) in polynomial time, every correct net should be obtainable from a sequent calculus proof, and there should be a cut-elimination procedure which preserves correctness.Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley [22], the author presented a calculus of proof nets satisfying and ; the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of . That sequent calculus, called LK⁎LK⁎ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper [22]), we give a full proof of for expansion nets with respect to LK⁎LK⁎, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria. (shrink)

Working memory is the system responsible for maintaining and manipulating information, in the face of ongoing distraction. In turn, WM span is perceived to be an individual-differences construct reflecting the limited capacity of this system. Recently, however, there has been some evidence to suggest that WM capacity can increase through training, raising the possibility that training can functionally alter the neural structures supporting WM. To address the hypothesis that the neural substrates underlying WM are targeted by training, we conducted a (...) meta-analysis of functional magnetic resonance imaging studies of WM training using Activation Likelihood Estimation. Our results demonstrate that WM training is associated exclusively with decreases in blood oxygenation level-dependent responses in clusters within the fronto-parietal system that underlie WM, including the bilateral inferior parietal lobule, middle and superior frontal gyri, and medial frontal gyrus bordering on the cingulate gyrus. We discuss the various psychological and physiological mechanisms that could be responsible for the observed reductions in the BOLD signal in relation to WM training, and consider their implications for the construct of WM span as a limited resource. (shrink)