Internationale Schiedsgerichtsbarkeit der Schweiz: vom Forum running zum judgment running?

Zum 65. Geburtstag von Prof. Dr. iur. et lic. oec. Heinrich Koller, haben über 40 Mitarbeiterinnen und Mitarbeiter des Bundesamtes für Justiz (BJ) eine Festschrift für ihren scheidenden Direktor verfasst. Die in deutscher und französischer Sprache verfassten Beiträge spiegeln das breite Spektrum einer Institution, aus deren «atelier» manch ein Gesetzesentwurf stammt. Oft übersehen wird dabei, dass das BJ aber auch eine «Werkstatt» ist, die das geltende Recht umsetzt und im Rahmen dieser Konkretisierung wichtige Akzente setzt. Die Festschrift bietet damit einen Blick hinter die Kulissen eines wichtigen Kompetenzzentrums für Rechtsfragen und beleuchtet aktuelle Probleme aus «erster Hand». Abgerundet wird die Festschrift mit einem Grusswort des Vorstehers EJPD (Bundesrat Christoph Blocher) und einem Schriftenverzeichnis von Heinrich Koller. Enthalten ist unter Anderem - die Bundesverfassung - weitere wichtige Gesetze und Verordnungen aus dem öffentlichen Recht - ZGB und Nebenerlasse - OR und Nebenerlasse - Erlasse zum Strafrecht und zur Strafrechtspflege - Gesetze zu Gesundheit, Arbeit und sozialer Sicherheit - wichtige Gesetze zu Wirtschaft und Kredit Autorinnen und Autoren Mitarbeiterinnen und Mitarbeiter des Bundesamtes für Justiz

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.

Children's and adolescent's self - assessment of metabolic control versus professional judgment: a cross-sectional retrospective and prospective cohort study

BACKGROUND Morbidity and mortality in T1DM depend on metabolic control, which is assessed by HbA1c measurements every 3-4 months. Patients' self-perception of glycemic control depends on daily blood glucose monitoring. Little is known about the congruence of patients' and professionals' perception of metabolic control in T1DM. OBJECTIVE To assess the actual patients' self-perception and objective assessment (HbA1c) of metabolic control in T1DM children and adolescents and to investigate the possible factors involved in any difference. METHODS Patients with T1DM aged 8 - 18 years were recruited in a cross-sectional, retrospective and prospective cohort study. Data collection consisted of clinical details, measured HbA1c, self-monitored blood glucose values and questionnaires assessing self and professionals' judgment of metabolic control. RESULTS 91 patients participated. Mean HbA1c was 8.03%. HbA1c was higher in patients with a diabetes duration > 2 years (p = 0.025) and in patients of lower socioeconomic level (p = 0.032). No significant correlation was found for self-perception of metabolic control in well and poorly controlled patients. We found a trend towards false-positive memory of the last HbA1c in patients with a HbA1c > 8.5% (p = 0.069) but no difference in patients' knowledge on target HbA1c between well and poorly controlled patients. CONCLUSIONS T1DM patients are aware of a target HbA1c representing good metabolic control. Ill controlled patients appear to have a poorer recollection of their HbA1c. Self-perception of actual metabolic control is similar in well and poorly controlled T1DM children and adolescents. Therefore, professionals should pay special attention that ill controlled T1DM patients perceive their HbA1c correctly.

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.