A Note on the Use of Sum in the Logic of Proofs

The Logic of Proofs~LP, introduced by Artemov, encodes the same reasoning as the modal logic~S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application~$\cdot$, positive introspection~!, and sum~+) are sufficient to mimic provability concealed in S4~modality. While the first two operations go back to G{\"o}del, the exact role of~+ remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP.

Transcatheter aortic valve implantation: the transfemoral access route is the default access

Transcatheter aortic valve implantation (TAVI) is a widely accepted alternative to surgical aortic valve replacement (SAVR) among non-operable patients or selected high-risk patients with degenerative, severe aortic stenosis. TAVI is considered less invasive when compared with SAVR; however, there remain significant differences between different TAVI access routes. The transfemoral approach is considered the least invasive access route, and can be performed as a fully percutaneous procedure in a spontaneously breathing patient under local anaesthesia and mild sedation only. Moreover, transfemoral TAVI patients are typically transferred to coronary care rather than to an intensive care unit after the procedure, and benefit from early ambulation and a reduction in overall length of hospital stay. Considering these patient-specific and health-economic advantages, several TAVI centres follow the least invasive strategy for their patients and have implemented the transfemoral access route as the default access in their institutions. This article provides an overview on the prerequisites for a successful transfemoral TAVI procedure, describes the procedural advantages compared to alternative access routes, and highlights differences in clinical outcomes.

Canonical proof nets for classical logic

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 (a) there should be a canonical function from sequent proofs to proof nets, (b) it should be possible to check the correctness of a net in polynomial time, (c) every correct net should be obtainable from a sequent calculus proof, and (d) 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 (2010) [22], the author presented a calculus of proof nets (expansion nets) satisfying (a) and (b); the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of (c). That sequent calculus, called LK∗ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper (a self-contained extended version of Richard McKinley (2010) [22]), we give a full proof of (c) for expansion nets with respect to 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.

Proof internalization in generalized Frege systems for classical logic

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.

Censors for Boolean Description Logic

Protecting different kinds of information has become an important area of research. One aspect is to provide effective means to avoid that secrets can be deduced from the answers of legitimate queries. In the context of atomic propositional databases several methods have been developed to achieve this goal. However, in those databases it is not possible to formalize structural information. Also they are quite restrictive with respect to the specification of secrets. In this paper we extend those methods to match the much greater expressive power of Boolean description logics. In addition to the formal framework, we provide a discussion of various kinds of censors and establish different levels of security they can provide.