View: session overviewtalk overview

Opening of CICM 2020

(Remark: All times mentioned in this program are in CEST (UTC+2))

13:00 | Towards a Heterogeneous Query Language for Mathematical Knowledge PRESENTER: Katja Berčič ABSTRACT. With more than 120.000 articles published annually in mathematical journals alone, mathematical search has often been touted as a killer application of computer-supported mathematics. But the artefacts of mathematics that should be searched are of very different natures such as mathematical documents, formulas, algorithms, concrete data sets, or semantic web--style graph abstractions. All are organized in complex ways and offer very different challenges and techniques for search. Therefore, existing representation languages and the corresponding query languages and search systems usually concentrate on only one of these aspects. As a consequence, each of these systems only partially covers the information needs of mathematical practitioners, and integrated solutions allowing multi-aspect queries are rare and basic. In this paper we present an architecture of a generic multi-aspect search system and evaluate it on paradigmatic examples of mathematical information needs. |

13:30 | OntoMathEdu: a New Linguistically Grounded Educational Mathematical Ontology PRESENTER: Alexander Kirillovich ABSTRACT. We present the first release of OntoMathEdu, a new educational mathematical ontology. The ontology is intended to be used as a Linked Open Data hub for mathematical education, a linguistic resource for intelligent mathematical language processing and an end-user reference educational database. The ontology is organized in three layers: a foundational ontology layer, a domain ontology layer and a linguistic layer. The domain ontology layer contains language-independent concepts, covering secondary school mathematics curriculum. The linguistic layer provides linguistic grounding for these concepts, and the foundation ontology layer provides them with meta-ontological annotations. The concepts are organized in two main hierarchies: the hierarchy of objects and the hierarchy of reified relationships. For our knowledge, OntoMathEdu is the first Linked Open Data mathematical ontology, that respects ontological distinctions provided by a foundational ontology; represents mathematical relationships as first-oder entities; and provides strong linguistic grounding for the represented mathematical concepts. |

14:00 | FrameIT: Detangling Knowledge Management from Game Design in Serious Games PRESENTER: Richard Marcus ABSTRACT. Serious games are an attempt to leverage the inherent motivation in game-like scenarios for an educational application and to transpose the learning goals into real-world applications. Unfortunately, serious games are also very costly to develop and deploy. For very abstract domains like mathematics, already the representation of the knowledge involved becomes a problem. We propose the FrameIT method that uses OMDoc/MMT theory graphs to represent and track the underlying knowledge in serious games. In this paper we report on an implementation and experiment that tests the method. We obtain a simple serious game by representing a ``word problem'' in OMDoc/MMT and connect the MMT API with a state-of-the-art game engine. |

16:30 | A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper) PRESENTER: Yassmeen Elderhalli ABSTRACT. Dependability analysis is an essential step in the design process of safety-critical systems, where the causes of failure and some other metrics, such as reliability, should be identified at an early design stage. The dynamic failure characteristics of real-world systems are usually captured by various dynamic dependability models, such as continuous time Markov chains (CTMCs), dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs). In order to conduct the formal dependability analysis of systems that exhibit dynamic failure behaviors, these models need to be captured formally. In this project paper, we describe recent developments towards this direction along with a roadmap on how to be able to develop a framework for formal reasoning support for DFTs, DRBDs and CTMCs in a higher-order-logic theorem prover. |

17:00 | Formal Adventures in Convex and Conical Spaces PRESENTER: Takafumi Saikawa ABSTRACT. Convex sets appear in various mathematical theories, and used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets in vector spaces, we formalize in Coq an intrinsic axiomatization of convex sets, namely convex spaces, based on an operation taking barycenters of points. A convex space corresponds to a specific type which does not refer to a surrounding vector space. This simplifies the definitions of functions on it. We show applications including the convexity of information-theoretic functions defined over types of distributions. We also show how convex spaces are embedded in conical spaces, which are abstract real cones, and use the embedding as an effective device to ease calculations. |

17:30 | Adding an Abstraction Barrier to ZF Set Theory PRESENTER: Ciaran Dunne ABSTRACT. Much mathematical writing exists that is, explicitly or implicitly, based on set theory, often Zermelo-Fraenkel set theory (ZF) or one of its variants. In ZF, the domain of discourse contains only sets, and hence every mathematical object must be a set. Consequently, in ZF, with the usual encoding of an ordered pair <a, b>, formulas like {a} ∈ <a, b> have truth values, and operations like P(<a, b>) have re- sults that are sets. Such ‘accidental theorems’ do not match how people think about the mathematics and also cause practical difficulties when using set theory in machine-assisted theorem proving. In contrast, in a number of proof assistants, mathematical objects and concepts can be built of type-theoretic stuff so that many mathematical objects can be, in essence, terms of an extended typed λ-calculus. However, dilemmas and frustration arise when formalizing mathematics in type theory. Motivated by problems of formalizing mathematics with (1) purely set-theoretic and (2) type-theoretic approaches, we explore an option with much of the flexibility of set theory and some of the useful features of type theory. We present ZFP: a modification of ZF that has ordered pairs as primitive, non-set objects. ZFP has a more natural and abstract axiomatic definition of ordered pairs free of any notion of representation. This paper presents axioms for ZFP, and a proof in ZF (machine-checked in Isabelle/ZF) of the existence of a model for ZFP, which implies that ZFP is consistent if ZF is. We discuss the approach used to add this abstraction barrier to ZF. |

18:00 | Formalizing Graph Trail Properties in Isabelle/HOL PRESENTER: Hanna Lachnitt ABSTRACT. We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of trails in weighted graphs. We do so by extending the graph theory library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one. |