The 2^nd International Conference on Artificial Intelligence Logic and Applications

Title: Temporal Cohort Logic

Guo-Qiang Zhang
Co-director for the Texas Institute for Restorative Neurotechnologies and UTHealth's Vice President and Chief Data Scientist
University of Texas, Houston, Texas, USA

Bio:Guo-Qiang ("GQ") Zhang is Professor of Medicine, Biomedical Informatics, and Public Health in the University of Texas Health Science Center at Houston (UTHealth Houston), Houston, Texas, USA. He serves as Co-director for the Texas Institute for Restorative Neurotechnologies and UTHealth's Vice President and Chief Data Scientist. Before joining UTHealth, he served as the inaugural director of the Institute for Biomedical Informatics, chief of the Division of Biomedical Informatics, and associate director of the Center for Clinical and Translational Science at the University of Kentucky. He spent prior years as a professor in the Case School of Engineering and School of Medicine at Case Western Reserve University, where he created its Division of Biomedical Informatics in the School of Medicine. GQ Zhang received his Ph.D.  in Computer Science from Cambridge University. His research spans data science, biomedical ontology development and quality assurance, clinical and research informatics, and agile, interface-driven, access-control-grounded software development. During the last decade, he led a research group that has developed production-strength, informatics tools for data capturing, data management, cohort discovery, and clinical decision support, resulting in over 200 scientific publications and multiple awards across the National Institutes of Health (NIH) institutes and the National Science Foundation (NSF).

Abstract:We introduce a new logic, called Temporal Cohort Logic (TCL), for cohort specification and discovery in clinical and population health research. TCL is created to fill a conceptual gap in formalizing temporal reasoning in biomedicine, in a similar role that temporal logics play for computer science and its applications. We provide formal syntax and semantics for TCL and illustrate the various logical constructs using examples related to human health. We then demonstrate possible further developments along the standard lines of logical enquiry about logical implication and equivalence, proof systems, soundness, completeness, expressiveness, decidability and computational complexity. Relationships and distinctions with existing temporal logic frameworks are discussed. Applications in electronic health record (EHR) and in neurophysiological data resource are provided. Our approach differs from existing temporal logics, in that we explicitly capture Allen's interval algebra as modal operators in a language of temporal logic (rather than addressing it purely in the semantic space). This has two major implications. First, it provides a formal logical framework for reasoning about time in biomedicine, allowing general (i.e., higher levels of abstraction) investigation into the properties of this framework independent of a specific query language or a database system. Second, it puts our approach in the context of logical developments in computer science (from the 70's to date), allowing the translation of existing results into the setting of TCL and its variants or subsystems so as to illuminate the opportunities and computational challenges involved in temporal reasoning for biomedicine.

Title: Qualitative Spatial and Temporal Reasoning

Sanjiang Li
Centre for Quantum Computation & Intelligent Systems (QCIS)
Faculty of Engineering and Information Technology
University of Technology, Sydney

Bio:Sanjiang Li received his B.Sc. and PhD in mathematics from Shaanxi Normal University in 1996 and Sichuan University in 2001. He is now a full professor in the Centre of Quantum Software & Information (QSI), Faculty of Engineering & Information Technology, University of Technology Sydney (UTS), Australia. Before joining UTS, he worked in the Computer Science and Technology Department, Tsinghua University, from September 2001 to December 2008. He was an Alexander von Humboldt research fellow at Freiburg University from January 2005 to June 2006; held a Microsoft Research Asia Young Professorship from July 2006 to June 2009; and an ARC Future Fellowship from January 2010 to December 2013.
His research interests are mainly in knowledge representation and artificial intelligence. The main objective of his previous research was to establish expressive representation formalism of spatial knowledge and provide effective reasoning mechanisms. Recently, he is also interested in research in quantum artificial intelligence. The aim is to develop quantum algorithms for solving AI problems and apply AI methods to solve classical problems in quantum computing. Some of his most important work has been published in international journals like Artificial Intelligence, IEEE TC, IEEE TCAD, ACM TODAES and international conferences like IJCAI, AAAI, KR, DAC, ICCAD.

Abstract:Spatial and temporal information is pervasive and increasingly involved in our everyday life. Many tasks in the real or virtual world require sophisticated spatial and temporal reasoning abilities. Qualitative Spatial and Temporal Reasoning (QSTR) has the potential to resolve the conflict between the abundance of spatial/temporal data and the scarcity of useful, human-comprehensible knowledge. The QSTR research aims to design (i) human-comprehensible and cognitively plausible spatial and temporal predicates (or query languages); and (ii) efficient algorithms for consistency checking (or query preprocessing). For intelligent systems, the ability to understand the qualitative, even vague, (textual or speech) information collected from either human beings or the Web is critical. This talk will introduce core notions and techniques developed in QSTR in the past three decades. I will focus on introducing Allen’s famous interval algebra and two well-known spatial relation models---the topological RCC8 algebra and the Cardinal Direction Calculus (CDC).

Title: Towards a Unifying Logical Framework for Neural Networks

Meng Sun
School of Mathematical Sciences, Peking University

Bio:Dr. Meng Sun is a full professor at School of Mathematical Sciences, Peking University since 2017. Prior to joining Peking University in 2010, he worked as a scientific staff member at CWI, the Netherlands, from 2006 to 2010, and as a postdoctoral researcher at National University of Singapore from 2005 to 2006. He received his PhD and BS degrees in applied mathematics from Peking University, in 2005 and 1999, respectively. His research interests mainly lie in software theory and formal methods in general, and in particular includes coordination models and languages, coalgebra theory and its applications, software verification and testing, cyber-physical systems, blockchain and smart contracts, theoretical foundation and certification techniques of deep learning systems. 

Abstract:Neural networks are increasingly used in safety-critical applications such as medical diagnosis and autonomous driving, which calls for the need for formal specification of their behaviors to guarantee their trustworthiness. In this work, we use matching logic---a unifying logic to specify and reason about programs and computing systems---to axiomatically define dynamic propagation and temporal operations in neural networks and to formally specify common properties about neural networks. As instances, we use matching logic to formalize a variety of neural networks, including generic feed-forward neural networks with different activation functions, convolutional neural networks and recurrent neural networks. We define their formal semantics and several common properties in matching logic. This way, we obtain a unifying logical framework for specifying neural networks and their properties.