A syntactic realization theorem for justification logics

Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms \$mathsfd\$, \$mathsft\$, \$mathsfb\$, \$mathsf4\$, and \$mathsf5\$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting's realization merging technique. We further strengthen the realization theorem for \$mathsfKB5\$ and \$mathsfS5\$ by showing that the positive introspection operator is superfluous.

Modal interpolation via nested sequents

The main method of proving the Craig Interpolation Property (CIP) constructively uses cut-free sequent proof systems. Until now, however, no such method has been known for proving the CIP using more general sequent-like proof formalisms, such as hypersequents, nested sequents, and labelled sequents. In this paper, we start closing this gap by presenting an algorithm for proving the CIP for modal logics by induction on a nested-sequent derivation. This algorithm is applied to all the logics of the so-called modal cube.

Proof theory for lattice-ordered groups

Proof-theoretic methods are developed and exploited to establish properties of the variety of lattice-ordered groups. In particular, a hypersequent calculus with a cut rule is used to provide an alternative syntactic proof of the generation of the variety by the lattice-ordered group of automorphisms of the real number chain. Completeness is also established for an analytic (cut-free) hypersequent calculus using cut elimination and it is proved that the equational theory of the variety is co-NP complete.

Survey of bluetongue virus infection in free-ranging wild ruminants in Switzerland.

BACKGROUND In 2006, bluetongue virus serotype 8 (BTV-8) was detected for the first time in central Europe. Measures to control the infection in livestock were implemented in Switzerland but the question was raised whether free-ranging wildlife could be a maintenance host for BTV-8. Furthermore Toggenburg orbivirus (TOV), considered as a potential 25th BTV serotype, was detected in 2007 in domestic goats in Switzerland and wild ruminants were considered a potential source of infection. To assess prevalences of BTV-8 and TOV infections in wildlife, we conducted a serological and virological survey in red deer, roe deer, Alpine chamois and Alpine ibex between 2009 and 2011. Because samples originating from wildlife carcasses are often of poor quality, we also documented the influence of hemolysis on test results, and evaluated the usefulness of confirmatory tests. RESULTS Ten out of 1,898 animals (0.5%, 95% confidence interval 0.3-1.0%) had detectable antibodies against BTV-8 and BTV-8 RNA was found in two chamois and one roe deer (0.3%, 0.1-0.8%). Seroprevalence was highest among red deer, and the majority of positive wild animals were sampled close to areas where outbreaks had been reported in livestock. Most samples were hemolytic and the range of the optical density percentage values obtained in the screening test increased with increasing hemolysis. Confirmatory tests significantly increased specificity of the testing procedure and proved to be applicable even on poor quality samples. Nearly all samples confirmed as positive had an optical density percentage value greater than 50% in the ELISA screening. CONCLUSIONS Prevalence of BTV-8 infection was low, and none of the tested animals were positive for TOV. Currently, wild ruminants are apparently not a reservoir for these viruses in Switzerland. However, we report for the first time BTV-8 RNA in Alpine chamois. This animal was found at high altitude and far from a domestic outbreak, which suggests that the virus could spread into/through the Alps. Regarding testing procedures, hemolysis did not significantly affect test results but confirmatory tests proved to be necessary to obtain reliable prevalence estimates. The cut-off value recommended by the manufacturer for the screening test was applicable for wildlife samples.