Masterarbeit, Otto-Friedrich-Universität Bamberg, 2025

This thesis presents a novel approach to clinical decision support in critical care by leveraging symbolic artificial intelligence (AI) for the formalization and automated verification of Spontaneous Breathing Trial (SBT) readiness assessments. It introduces a prototype system that transforms Intensive Care Unit (ICU) checklist logic into machine-verifiable higher-order logic (HOL) using Isabelle/HOL, ensuring correctness-by-construction, traceability, and semantic fidelity. The system was implemented in Java and supports modular, extensible workflows encompassing Health Level 7 (HL7)-compatible data ingestion, logic generation, and automated proof execution. A simulated environment was used to evaluate the prototype’s performance across clinical and technical dimensions. Results demonstrate consistent and explainable classifications aligned with clinical expectations, and profiling indicates linear scalability with respect to patient count and checklist complexity. Qualitative analysis highlights the system’s interpretability, workflow compatibility, and auditability. Limitations concerning real-world integration, proof traceability, and regulatory readiness are critically examined. The work establishes a reusable methodology for the formalization of protocol-based reasoning and outlines future directions including live deployment, integration with subsymbolic models, and regulatory certification. This research contributes a technically sound and ethically aligned foundation for the development of transparent, verifiable, and adaptable AI systems in healthcare.