Keynote Speeches
Title: Logic for Reinforcement Learning
Natasha Alechina
Open University of Netherlands and Flanders
Abstract:
Temporal logic is increasingly used in Reinforcement Learning to give a declarative specification of a task to be learned (and avoid problems with reward gaming and other challenges of reward functions) and to specify declarative constraints on agents’ behaviour (in particular, safety constraints). I will talk about recent work in this area.
Title: Extending Hoare logic to hybrid systems
Naijun Zhan
Peking University, School of Computer Science
Abstract:
In this talk, I will talk our efforts on extending Hoare logic to hybrid systems, named hybrid Hoare logic, including two versions: a DC-based version and and a generalized version without DC. I will briefly introduce the DC-based version, and mainly focus on the second version. I will explain why we need a generalized version, and present its proof system, the soundness and discrete and continuous relative completeness of the proof system, the implementation of an interactive theorem prover based on Isabelle/HLL called HHLProver, the automation of HHLProver, and finally introduce some applications with the logic and its prover.
Title: Ensemble Logic: a Unified Framework for Temporal, Spatial, and Spatial-Temporal Reasoning
Guo-Qiang Zhang
The University of Texas Health Science Center at Houston
Before joining UTHealth, he served as the inaugural director for the Institute for Biomedical Informatics, chief of the Division of Biomedical Informatics, and associate director for the Center for Clinical and Translational Science (CTSA) at the University of Kentucky. He spent prior years as a faculty member at 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 while serving as its CTSA informatics core director.
GQ Zhang received his Ph.D. in Computer Science from Cambridge University. His research work and interests span data ecosystems and big data, biomedical ontology development and quality assurance, clinical and research informatics, and data coordination systems for prospective metadata management in national consortia, such as the latest, on-going NIH BRAIN Initiative Cell Atlas Network (BICAN). He has launched a research program called Logic-based Phenotyping, a formalized mathematical approach for temporal phenotype representation and reasoning using an expressive and purpose-fitting framework called Temporal Ensemble Logic. His work has been funded by research awards from the National Institutes of Health (NIH) and the National Science Foundation (NSF) of the United States.
Abstract:
I introduced Temporal ensemble logic (TEL;
arXiv:2408.14443
) a year ago to fill a gap in formal languages for capturing phenotypes in biomedicine. TEL combines first-order logic and modal logic constructs as primitives in a novel setup that is more expressive than existing linear-time temporal logic. In this presentation I will cover the latest development in this area, with motivating examples and expressiveness results in terms of language classes and undecidability properties, and introduce Ensemble Logic (EL) as a generalized, unified framework for (1) temporal, (2) spatial, and (3) spatial-temporal reasoning on any mathematical space consisting of a monoid with a distance measure or an order relation,
such as real numbers (
ℝ
), integers (
ℕ
), and Euclidian spaces (
ℝn
).
Title: A Formal Semantics for Generic Sentences and Metaphorical Sentences
Beihai Zhou
School of Philosophy, Shanxi University
Abstract:
Generic sentences are sentences such as “Birds can fly”. Generic sentences are sentences that express the characteristic attributes of things. They are universal and at the same time tolerate exceptions. This characteristic is one of the fundamental reasons for the non - monotonicity of reasoning. Therefore, the logic of generic sentences is also a non - monotonic logic. The formal characterization of the reasoning of generic sentences was first proposed by default logic. There are various different understandings of generic sentences, and multiple formal characterization schemes have also emerged. These understandings and characterizations all have their own problems. This study argues that generic sentences are sentences that express the connotations of everyday concepts, and based on this, a formal semantics for generic sentences is provided. The formal semantics of generic sentences has two aspects of significance: on the one hand, it is an intermediary connecting intuitive analysis and formal characterization. Starting from the basic understanding of generic sentences, through this intermediary, one can then move on to the formal characterization of the logic of generic sentences; on the other hand, there is a natural connection between generic sentences and metaphorical sentences. If a formal semantics correctly characterizes generic sentences, then it should be able to be extended to metaphorical sentences. It is precisely based on this view that the formal semantics of generic sentences provided in this study is then extended to metaphorical sentences. The success of this extension in turn confirms the rationality of understanding generic sentences based on everyday concepts.
