A Finite Model Property for Gödel Modal Logics

A new semantics with the finite model property is provided and used to establish decidability for Gödel modal logics based on (crisp or fuzzy) Kripke frames combined locally with Gödel logic. A similar methodology is also used to establish decidability, and indeed co-NP-completeness for a Gödel S5 logic that coincides with the one-variable fragment of first-order Gödel logic.

A Portable Image Overlay Projection Device for Computer-Aided Open Liver Surgery

Image overlay projection is a form of augmented reality that allows surgeons to view underlying anatomical structures directly on the patient surface. It improves intuitiveness of computer-aided surgery by removing the need for sight diversion between the patient and a display screen and has been reported to assist in 3-D understanding of anatomical structures and the identification of target and critical structures. Challenges in the development of image overlay technologies for surgery remain in the projection setup. Calibration, patient registration, view direction, and projection obstruction remain unsolved limitations to image overlay techniques. In this paper, we propose a novel, portable, and handheld-navigated image overlay device based on miniature laser projection technology that allows images of 3-D patient-specific models to be projected directly onto the organ surface intraoperatively without the need for intrusive hardware around the surgical site. The device can be integrated into a navigation system, thereby exploiting existing patient registration and model generation solutions. The position of the device is tracked by the navigation system’s position sensor and used to project geometrically correct images from any position within the workspace of the navigation system. The projector was calibrated using modified camera calibration techniques and images for projection are rendered using a virtual camera defined by the projectors extrinsic parameters. Verification of the device’s projection accuracy concluded a mean projection error of 1.3 mm. Visibility testing of the projection performed on pig liver tissue found the device suitable for the display of anatomical structures on the organ surface. The feasibility of use within the surgical workflow was assessed during open liver surgery. We show that the device could be quickly and unobtrusively deployed within the sterile environment.

Influence of Smoothing on Voxel-Based Mesh Accuracy in Micro-Finite Element

The interest in automatic volume meshing for finite element analysis (FEA) has grown more since the appearance of microfocus CT (μCT), due to its high resolution, which allows for the assessment of mechanical behaviour at a high precision. Nevertheless, the basic meshing approach of generating one hexahedron per voxel produces jagged edges. To prevent this effect, smoothing algorithms have been introduced to enhance the topology of the mesh. However, whether smoothing also improves the accuracy of voxel-based meshes in clinical applications is still under question. There is a trade-off between smoothing and quality of elements in the mesh. Distorted elements may be produced by excessive smoothing and reduce accuracy of the mesh. In the present work, influence of smoothing on the accuracy of voxel-based meshes in micro-FE was assessed. An accurate 3D model of a trabecular structure with known apparent mechanical properties was used as a reference model. Virtual CT scans of this reference model (with resolutions of 16, 32 and 64 μm) were then created and used to build voxel-based meshes of the microarchitecture. Effects of smoothing on the apparent mechanical properties of the voxel-based meshes as compared to the reference model were evaluated. Apparent Young’s moduli of the smooth voxel-based mesh were significantly closer to those of the reference model for the 16 and 32 μm resolutions. Improvements were not significant for the 64 μm, due to loss of trabecular connectivity in the model. This study shows that smoothing offers a real benefit to voxel-based meshes used in micro-FE. It might also broaden voxel-based meshing to other biomechanical domains where it was not used previously due to lack of accuracy. As an example, this work will be used in the framework of the European project ContraCancrum, which aims at providing a patient-specific simulation of tumour development in brain and lungs for oncologists. For this type of clinical application, such a fast, automatic, and accurate generation of the mesh is of great benefit.

Mesh-based vs. Image-based Statistical Appearance Model of the Human Femur: a Preliminary Comparison Study for the Creation of Finite Element Meshes

Statistical models have been recently introduced in computational orthopaedics to investigate the bone mechanical properties across several populations. A fundamental aspect for the construction of statistical models concerns the establishment of accurate anatomical correspondences among the objects of the training dataset. Various methods have been proposed to solve this problem such as mesh morphing or image registration algorithms. The objective of this study is to compare a mesh-based and an image-based statistical appearance model approaches for the creation of nite element(FE) meshes. A computer tomography (CT) dataset of 157 human left femurs was used for the comparison. For each approach, 30 finite element meshes were generated with the models. The quality of the obtained FE meshes was evaluated in terms of volume, size and shape of the elements. Results showed that the quality of the meshes obtained with the image-based approach was higher than the quality of the mesh-based approach. Future studies are required to evaluate the impact of this finding on the final mechanical simulations.

Statistical finite element model for bone shape and biomechanical properties

We present a framework for statistical finite element analysis combining shape and material properties, and allowing performing statistical statements of biomechanical performance across a given population. In this paper, we focus on the design of orthopaedic implants that fit a maximum percentage of the target population, both in terms of geometry and biomechanical stability. CT scans of the bone under consideration are registered non-rigidly to obtain correspondences in position and intensity between them. A statistical model of shape and intensity (bone density) is computed by means of principal component analysis. Afterwards, finite element analysis (FEA) is performed to analyse the biomechanical performance of the bones. Realistic forces are applied on the bones and the resulting displacement and bone stress distribution are calculated. The mechanical behaviour of different PCA bone instances is compared.

A nonlinear QCT-based finite element model validation study for the human femur tested in two configurations in vitro

Purpose Femoral fracture is a common medical problem in osteoporotic individuals. Bone mineral density (BMD) is the gold standard measure to evaluate fracture risk in vivo. Quantitative computed tomography (QCT)-based homogenized voxel finite element (hvFE) models have been proved to be more accurate predictors of femoral strength than BMD by adding geometrical and material properties. The aim of this study was to evaluate the ability of hvFE models in predicting femoral stiffness, strength and failure location for a large number of pairs of human femora tested in two different loading scenarios. Methods Thirty-six pairs of femora were scanned with QCT and total proximal BMD and BMC were evaluated. For each pair, one femur was positioned in one-legged stance configuration (STANCE) and the other in a sideways configuration (SIDE). Nonlinear hvFE models were generated from QCT images by reproducing the same loading configurations imposed in the experiments. For experiments and models, the structural properties (stiffness and ultimate load), the failure location and the motion of the femoral head were computed and compared. Results In both configurations, hvFE models predicted both stiffness (R2=0.82 for STANCE and R2=0.74 for SIDE) and femoral ultimate load (R2=0.80 for STANCE and R2=0.85 for SIDE) better than BMD and BMC. Moreover, the models predicted qualitatively well the failure location (66% of cases) and the motion of the femoral head. Conclusions The subject specific QCT-based nonlinear hvFE model cannot only predict femoral apparent mechanical properties better than densitometric measures, but can additionally provide useful qualitative information about failure location.

Comparison of theoretical fixation stability of three devices employed in medial opening wedge high tibial osteotomy: a finite element analysis.

BACKGROUND Medial open wedge high tibial osteotomy is a well-established procedure for the treatment of unicompartmental osteoarthritis and symptomatic varus malalignment. We hypothesized that different fixation devices generate different fixation stability profiles for the various wedge sizes in a finite element (FE) analysis. METHODS Four types of fixation were compared: 1) first and 2) second generation Puddu plates, and 3) TomoFix plate with and 4) without bone graft. Cortical and cancellous bone was modelled and five different opening wedge sizes were studied for each model. Outcome measures included: 1) stresses in bone, 2) relative displacement of the proximal and distal tibial fragments, 3) stresses in the plates, 4) stresses on the upper and lower screw surfaces in the screw channels. RESULTS The highest load for all fixation types occurred in the plate axis. For the vast majority of the wedge sizes and fixation types the shear stress (von Mises stress) was dominating in the bone independent of fixation type. The relative displacements of the tibial fragments were low (in μm range). With an increasing wedge size this displacement tended to increase for both Puddu plates and the TomoFix plate with bone graft. For the TomoFix plate without bone graft a rather opposite trend was observed.For all fixation types the occurring stresses at the screw-bone contact areas pulled at the screws and exceeded the allowable threshold of 1.2 MPa for at least one screw surface. Of the six screw surfaces that were studied, the TomoFix plate with bone graft showed a stress excess of one out of twelve and without bone graft, five out of twelve. With the Puddu plates, an excess stress occurred in the majority of screw surfaces. CONCLUSIONS The different fixation devices generate different fixation stability profiles for different opening wedge sizes. Based on the computational simulations, none of the studied osteosynthesis fixation types warranted an intransigent full weight bearing per se. The highest fixation stability was observed for the TomoFix plates and the lowest for the first generation Puddu plate. These findings were revealed in theoretical models and need to be validated in controlled clinical settings.

Generation of a murine hepatic angiosarcoma cell line and reproducible mouse tumor model

Hepatic angiosarcoma (AS) is a rare and highly aggressive tumor of endothelial origin with dismal prognosis. Studies of the molecular biology of AS and treatment options are limited as animal models are rare. We have previously shown that inducible knockout of Notch1 in mice leads to spontaneous formation of hepatic AS. The aims of this study were to: (1) establish and characterize a cell line derived from this murine AS, (2) identify molecular pathways involved in the pathogenesis and potential therapeutic targets, and (3) generate a tumor transplantation model. AS cells retained specific endothelial properties such as tube formation activity, as well as expression of CD31 and Von Willebrand factor. However, electron microscopy analysis revealed signs of dedifferentiation with loss of fenestrae and loss of contact inhibition. Microarray and pathway analysis showed substantial changes in gene expression and revealed activation of the Myc pathway. Exposing the AS cells to sorafenib reduced migration, filopodia dynamics, and cell proliferation but did not induce apoptosis. In addition, sorafenib suppressed ERK phosphorylation and expression of cyclin D2. Injection of AS cells into NOD/SCID mice resulted in formation of undifferentiated tumors, confirming the tumorigenic potential of these cells. In summary, we established and characterized a murine model of spontaneous AS formation and hepatic AS cell lines as a useful in vitro tool. Our data demonstrate antitumor activity of sorafenib in AS cells with potent inhibition of migration, filopodia formation, and cell proliferation, supporting further evaluation of sorafenib as a novel treatment strategy. In addition, AS cell transplantation provides a subcutaneous tumor model useful for in vivo preclinical drug testing.Laboratory Investigation advance online publication, 24 November 2014; doi:10.1038/labinvest.2014.141.

Improving residency training with the help of multisource feedback: Generation of a model of influencing factors

Background: Feedback is considered to be one of the most important drivers of learning. One form of structured feedback used in medical settings is multisource feedback (MSF). This feedback technique provides the opportunity to gain a differentiated view on a doctor’s performance from several perspectives using a questionnaire and a facilitating conversation, in which learning goals are formulated. While many studies have been conducted on the validity, reliability and feasibility of the instrument, little is known about the impact of factors that might influence the effects of MSF on clinical performance. Summary of Work: To study under which circumstances MSF is most effective, we performed a literature review on Google Scholar with focus on MSF and feedback in general. Main key-words were: MSF, multi-source-feedback, multi source feedback, and feedback each combined with influencing/ hindering/ facilitating factors, effective, effectiveness, doctors-intraining, and surgery. Summary of Results: Based on the literature, we developed a preliminary model of facilitating factors. This model includes five main factors influencing MSF: questionnaire, doctor-in-training, group of raters, facilitating supervisor, and facilitating conversation. Discussion and Conclusions: Especially the following points that might influence MSF have not yet been sufficiently studied: facilitating conversation with the supervisor, individual aspects of doctors-in-training, and the causal relations between influencing factors. Overall there are only very few studies focusing on the impact of MSF on actual and long-term performance. We developed a preliminary model of hindering and facilitating factors on MSF. Further studies are needed to better understand under which circumstances MSF is most effective. Take-home messages: The preliminary model might help to guide further studies on how to implement MSF to use it at its full potential.