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.

Design and Realization of an Energy Harvester Using Pulsating Arterial Pressure

Most medical implants run on batteries, which require costly and tedious replacement or recharging. It is believed that micro-generators utilizing intracorporeal energy could solve these problems. However, such generators do not, at this time, meet the energy requirements of medical implants.This paper highlights some essential aspects of designing and implementing a power source that scavenges energy from arterial expansion and contraction to operate an implanted medical device. After evaluating various potentially viable transduction mechanisms, the fabricated prototype employs an electromagnetic transduction mechanism. The artery is inserted into a laboratory-fabricated flexible coil which is permitted to freely deform in a magnetic field. This work also investigates the effects of the arterial wall's material properties on energy harvesting potential. For that purpose, two types of arteries (Penrose X-ray tube, which behave elastically, and an artery of a Göttinger minipig, which behaves viscoelastically) were tested. No noticeable difference could be observed between these two cases. For the pig artery, average harvestable power was 42 nW. Moreover, peak power was 2.38 μW. Both values are higher than those of the current state of the art (6 nW/16 nW). A theoretical modelling of the prototype was developed and compared to the experimental results.