In modern dynamic constantly developing society, more and more people suffer from chronic and serious diseases and doctors and patients need special and sophisticated medical and health support. Accordingly, prominent health stakeholders have recognized the importance of development of such services to make patients' life easier. Such support requires the collection of: huge amount of patients' complex data (clinical, environmental, nutritional, daily activities), variety of data from smart wearable devices, data from clothing equipped with sensors etc. Holistic patient's data must be properly aggregated, processed, analyzed, and presented to the doctors/caregivers to recommend adequate treatment and actions to improve patient's health related parameters and general wellbeing. Advanced artificial intelligence techniques offer the opportunity to analyze such big data, consume them, and derive new knowledge to support (personalized) medical decisions. New approaches like those based on advanced machine/deep learning, federated learning, transfer learning, explainable artificial intelligence open new paths for more quality use of health and medical data in future. In this paper, we will present some crucial aspects and characteristic examples in the area of application of a range of artificial intelligence approaches in (personalized) medical decisions.

We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the well-known correction of Herbrand's False Lemma by Goedel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand's Modus Ponens Elimination. Besides Herbrand's Fundamental Theorem and its relation to the Loewenheim-Skolem-Theorem, we carefully investigate Herbrand's notion of intuitionism in connection with his notion of falsehood in an infinite domain. We sketch Herbrand's two proofs of the consistency of arithmetic and his notion of a recursive function, and last but not least, present the correct original text of his unification algorithm with a new translation.

Computer-supported learning is an increasingly important form of study since it allows for independent learning and individualized instruction. In this paper, we discuss a novel approach to developing an intelligent tutoring system for teaching textbook-style mathematical proofs. We characterize the particularities of the domain and discuss common ITS design models. Our approach is motivated by phenomena found in a corpus of tutorial dialogs that were collected in a Wizard-of-Oz experiment. We show how an intelligent tutor for textbook-style mathematical proofs can be built on top of an adapted assertion-level proof assistant by reusing representations and proof search strategies originally developed for automated and interactive theorem proving. The resulting prototype was successfully evaluated on a corpus of tutorial dialogs and yields good results.