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.

Lower complexity bounds in justification logic

Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in~NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound. The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are $\Pi^p_2$-hard, reproving and generalizing an earlier result by Milnikel.

SWISSspine: a nationwide registry for health technology assessment of lumbar disc prostheses

SWISSspine is a so-called pragmatic trial for assessment of safety and efficiency of total disc arthroplasty (TDA). It follows the new health technology assessment (HTA) principle of "coverage with evidence development". It is the first mandatory HTA registry of its kind in the history of Swiss orthopaedic surgery. Its goal is the generation of evidence for a decision by the Swiss federal office of health about reimbursement of the concerned technologies and treatments by the basic health insurance of Switzerland. During the time between March 2005 and 2008, 427 interventions with implantation of 497 lumbar total disc arthroplasties have been documented. Data was collected in a prospective, observational multicenter mode. The preliminary timeframe for the registry was 3 years and has already been extended. Data collection happens pre- and perioperatively, at the 3 months and 1-year follow-up and annually thereafter. Surgery, implant and follow-up case report forms are administered by spinal surgeons. Comorbidity questionnaires, NASS and EQ-5D forms are completed by the patients. Significant and clinically relevant reduction of low back pain VAS (70.3-29.4 points preop to 1-year postop, p < 0.0001) leg pain VAS (55.5-19.1 points preop to 1-year postop, p < 0.001), improvement of quality of life (EQ-5D, 0.32-0.73 points preop to 1-year postop, p < 0.001) and reduction of pain killer consumption was revealed at the 1-year follow-up. There were 14 (3.9%) complications and 7 (2.0%) revisions within the same hospitalization reported for monosegmental TDA; there were 6 (8.6%) complications and 8 (11.4%) revisions for bisegmental surgery. There were 35 patients (9.8%) with complications during followup in monosegmental and 9 (12.9%) in bisegmental surgery and 11 (3.1%) revisions with 1 [corrected] new hospitalization in monosegmental and 1 (1.4%) in bisegmental surgery. Regression analysis suggested a preoperative VAS "threshold value" of about 44 points for increased likelihood of a minimum clinically relevant back pain improvement. In a short-term perspective, lumbar TDA appears as a relatively safe and efficient procedure concerning pain reduction and improvement of quality of life. Nevertheless, no prediction about the long-term goals of TDA can be made yet. The SWISSspine registry proofs to be an excellent tool for collection of observational data in a nationwide framework whereby advantages and deficits of its design must be considered. It can act as a model for similar projects in other health-care domains.

Amalgamation and interpolation in ordered algebras

The first part of this paper provides a comprehensive and self-contained account of the interrelationships between algebraic properties of varieties and properties of their free algebras and equational consequence relations. In particular, proofs are given of known equivalences between the amalgamation property and the Robinson property, the congruence extension property and the extension property, and the flat amalgamation property and the deductive interpolation property, as well as various dependencies between these properties. These relationships are then exploited in the second part of the paper in order to provide new proofs of amalgamation and deductive interpolation for the varieties of lattice-ordered abelian groups and MV-algebras, and to determine important subvarieties of residuated lattices where these properties hold or fail. In particular, a full description is given of all subvarieties of commutative GMV-algebras possessing the amalgamation property.

Service-centric Networking Extensions

This paper discusses several issues of Service-Centric Networking (SCN) as an extension of the Information-Centric Networking (ICN) paradigm. SCN allows extended caching, where not exactly the same content as requested can be read from caches, but similar content can be used to produce the content requested, e.g., by filtering or transcoding. We discuss the issue of naming and routing for general dynamic services for both tightly coupled and decoupled ICN approaches. Challenges and solutions for service management are identified, in particular for composed services, which allow distributed in-network processing of service requests. We introduce the term Software-Defined Service-Centric Networking as an extension of Software-Defined Networking. A prototype implementation for SCN proofs its validity and feasibility and underlines its potential benefits.

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.

Good just isn't Good Enough: Humean Chances and Boltzmannian Statistical Physics

Statistical physicists assume a probability distribution over micro-states to explain thermodynamic behavior. The question of this paper is whether these probabilities are part of a best system and can thus be interpreted as Humean chances. I consider two Boltzmannian accounts of the Second Law, viz.\ a globalist and a localist one. In both cases, the probabilities fail to be chances because they have rivals that are roughly equally good. I conclude with the diagnosis that well-defined micro-probabilities under-estimate the robust character of explanations in statistical physics.

Sheaf representations of MV-algebras and lattice-ordered abelian groups via duality

We study representations of MV-algebras -- equivalently, unital lattice-ordered abelian groups -- through the lens of Stone-Priestley duality, using canonical extensions as an essential tool. Specifically, the theory of canonical extensions implies that the (Stone-Priestley) dual spaces of MV-algebras carry the structure of topological partial commutative ordered semigroups. We use this structure to obtain two different decompositions of such spaces, one indexed over the prime MV-spectrum, the other over the maximal MV-spectrum. These decompositions yield sheaf representations of MV-algebras, using a new and purely duality-theoretic result that relates certain sheaf representations of distributive lattices to decompositions of their dual spaces. Importantly, the proofs of the MV-algebraic representation theorems that we obtain in this way are distinguished from the existing work on this topic by the following features: (1) we use only basic algebraic facts about MV-algebras; (2) we show that the two aforementioned sheaf representations are special cases of a common result, with potential for generalizations; and (3) we show that these results are strongly related to the structure of the Stone-Priestley duals of MV-algebras. In addition, using our analysis of these decompositions, we prove that MV-algebras with isomorphic underlying lattices have homeomorphic maximal MV-spectra. This result is an MV-algebraic generalization of a classical theorem by Kaplansky stating that two compact Hausdorff spaces are homeomorphic if, and only if, the lattices of continuous [0, 1]-valued functions on the spaces are isomorphic.

A Logical Descriptor for Regular Languages via Stone Duality

In this paper we introduce a class of descriptors for regular languages arising from an application of the Stone duality between finite Boolean algebras and finite sets. These descriptors, called classical fortresses, are object specified in classical propositional logic and capable to accept exactly regular languages. To prove this, we show that the languages accepted by classical fortresses and deterministic finite automata coincide. Classical fortresses, besides being propositional descriptors for regular languages, also turn out to be an efficient tool for providing alternative and intuitive proofs for the closure properties of regular languages.

M-Functionals of Multivariate Scatter

This survey provides a self-contained account of M-estimation of multivariate scatter. In particular, we present new proofs for existence of the underlying M-functionals and discuss their weak continuity and differentiability. This is done in a rather general framework with matrix-valued random variables. By doing so we reveal a connection between Tyler's (1987) M-functional of scatter and the estimation of proportional covariance matrices. Moreover, this general framework allows us to treat a new class of scatter estimators, based on symmetrizations of arbitrary order. Finally these results are applied to M-estimation of multivariate location and scatter via multivariate t-distributions.

hp-DGFEM for second-order mixed elliptic problems polyhedra

We prove exponential rates of convergence of hp-version discontinuous Galerkin (dG) interior penalty finite element methods for second-order elliptic problems with mixed Dirichlet-Neumann boundary conditions in axiparallel polyhedra. The dG discretizations are based on axiparallel, σ-geometric anisotropic meshes of mapped hexahedra and anisotropic polynomial degree distributions of μ-bounded variation. We consider piecewise analytic solutions which belong to a larger analytic class than those for the pure Dirichlet problem considered in [11, 12]. For such solutions, we establish the exponential convergence of a nonconforming dG interpolant given by local L 2 -projections on elements away from corners and edges, and by suitable local low-order quasi-interpolants on elements at corners and edges. Due to the appearance of non-homogeneous, weighted norms in the analytic regularity class, new arguments are introduced to bound the dG consistency errors in elements abutting on Neumann edges. The non-homogeneous norms also entail some crucial modifications of the stability and quasi-optimality proofs, as well as of the analysis for the anisotropic interpolation operators. The exponential convergence bounds for the dG interpolant constructed in this paper generalize the results of [11, 12] for the pure Dirichlet case.