Forcing for hat inductive definitions in arithmetic

By forcing, we give a direct interpretation of inline image into Avigad's inline image. To the best of the author's knowledge, this is one of the simplest applications of forcing to “real problems”.

Unfolding Feasible Arithmetic and Weak Truth

In this paper we continue Feferman’s unfolding program initiated in (Feferman, vol. 6 of Lecture Notes in Logic, 1996) which uses the concept of the unfolding U(S) of a schematic system S in order to describe those operations, predicates and principles concerning them, which are implicit in the acceptance of S. The program has been carried through for a schematic system of non-finitist arithmetic NFA in Feferman and Strahm (Ann Pure Appl Log, 104(1–3):75–96, 2000) and for a system FA (with and without Bar rule) in Feferman and Strahm (Rev Symb Log, 3(4):665–689, 2010). The present contribution elucidates the concept of unfolding for a basic schematic system FEA of feasible arithmetic. Apart from the operational unfolding U0(FEA) of FEA, we study two full unfolding notions, namely the predicate unfolding U(FEA) and a more general truth unfolding UT(FEA) of FEA, the latter making use of a truth predicate added to the language of the operational unfolding. The main results obtained are that the provably convergent functions on binary words for all three unfolding systems are precisely those being computable in polynomial time. The upper bound computations make essential use of a specific theory of truth TPT over combinatory logic, which has recently been introduced in Eberhard and Strahm (Bull Symb Log, 18(3):474–475, 2012) and Eberhard (A feasible theory of truth over combinatory logic, 2014) and whose involved proof-theoretic analysis is due to Eberhard (A feasible theory of truth over combinatory logic, 2014). The results of this paper were first announced in (Eberhard and Strahm, Bull Symb Log 18(3):474–475, 2012).

Dynamic computer simulations of electrophoresis: a versatile research and teaching tool

Software is available, which simulates all basic electrophoretic systems, including moving boundary electrophoresis, zone electrophoresis, ITP, IEF and EKC, and their combinations under almost exactly the same conditions used in the laboratory. These dynamic models are based upon equations derived from the transport concepts such as electromigration, diffusion, electroosmosis and imposed hydrodynamic buffer flow that are applied to user-specified initial distributions of analytes and electrolytes. They are able to predict the evolution of electrolyte systems together with associated properties such as pH and conductivity profiles and are as such the most versatile tool to explore the fundamentals of electrokinetic separations and analyses. In addition to revealing the detailed mechanisms of fundamental phenomena that occur in electrophoretic separations, dynamic simulations are useful for educational purposes. This review includes a list of current high-resolution simulators, information on how a simulation is performed, simulation examples for zone electrophoresis, ITP, IEF and EKC and a comprehensive discussion of the applications and achievements.

Computer-assisted design and manufacture of implants in the late reconstruction of extensive orbital fractures

To evaluate the use of computer-assisted designed and manufactured (CAD/CAM) orbital wall and floor implants for late reconstruction of extensive orbital fractures.

Improved detection of pulmonary nodules on energy-subtracted chest radiographs with a commercial computer-aided diagnosis software: comparison with human observers

To retrospectively analyze the performance of a commercial computer-aided diagnosis (CAD) software in the detection of pulmonary nodules in original and energy-subtracted (ES) chest radiographs.

Computer Aided Surgery for Percutaneous Nephrolithotomy: Clinical Requirement Analysis and System Design

Percutaneous nephrolithotomy (PCNL) for the treatment of renal stones and other related renal diseases has proved its efficacy and has stood the test of time compared with open surgical methods and extracorporal shock wave lithotripsy. However, access to the collecting system of the kidney is not easy because the available intra-operative image modalities only provide a two dimensional view of the surgical scenario. With this lack of visual information, several punctures are often necessary which, increases the risk of renal bleeding, splanchnic, vascular or pulmonary injury, or damage to the collecting system which sometimes makes the continuation of the procedure impossible. In order to address this problem, this paper proposes a workflow for introduction of a stereotactic needle guidance system for PCNL procedures. An analysis of the imposed clinical requirements, and a instrument guidance approach to provide the physician with a more intuitive planning and visual guidance to access the collecting system of the kidney are presented.

Radiation dose reduction in computer assisted navigation for functional endoscopic sinus surgery--cadaver head experiments and clinical implementation

Computed tomography based navigation for endoscopic sinus surgery is inflationary used despite of major public concern about iatrogenic radiation induced cancer risk. Studies on dose reduction for CAS-CT are almost nonexistent. We validate the use of radiation dose reduced CAS-CT for clinically applied surface registration.