ASCAPE: An open AI ecosystem to support the quality of life of cancer patients

The latest cancer statistics indicate a decrease in cancer-related mortality. However, due to the growing and ageing population, the absolute number of people living with cancer is set to keep increasing. This paper presents ASCAPE, an open AI infrastructure that takes advantage of the recent advances in Artificial Intelligence (AI) and Machine Learning (ML) to support cancer patients quality of life (QoL). With ASCAPE health stakeholders (e.g. hospitals) can locally process their private medical data and then share the produced knowledge (ML models) through the open AI infrastructure.

AI Approaches in Processing and Using Data in Personalized Medicine

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 like clinical, environmental, nutritional, daily activities, variety of data from smart wearable devices, data from clothing equipped with sensors etc. Holistic patients data must be properly aggregated, processed, analyzed, and presented to the doctors and caregivers to recommend adequate treatment and actions to improve patients 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 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.

Proceedings of the 12th Workshop on User Interfaces for Theorem Provers

The UITP workshop series brings together researchers interested in designing, developing and evaluating user interfaces for automated reasoning tools, such as interactive proof assistants, automated theorem provers, model finders, tools for formal methods, and tools for visualising and manipulating logical formulas and proofs. The twelth edition of UITP took place in Coimbra, Portugal, and was part of the International Joint Conference on Automated Reasoning (IJCAR'16). The workshop consisted of an invited talk, six presentations of submitted papers and lively hands-on session for reasoning tools and their user-interface. These post-proceedings contain four contributed papers accepted for publication after a second round of reviewing after the workshop as well as the invited paper.

Structure Formation in Large Theories

Structuring theories is one of the main approaches to reduce the combinatorial explosion associated with reasoning and exploring large theories. In the past we developed the notion of development graphs as a means to represent and maintain structured theories. In this paper we present a methodology and a resulting implementation to reveal the hidden structure of flat theories by transforming them into detailed development graphs. We review our approach using plain TSTP-representations of MIZAR articles obtaining more structured and also more concise theories.

Lectures on Jacques Herbrand as a Logician

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.

Towards an Intelligent Tutor for Mathematical Proofs

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.