View: session overviewtalk overview

Regular papers

13:00 | A Language with Type-Dependent Equality ABSTRACT. Most formal systems use equality as an absolute property in the sense that two objects are equal or not. Even the ternary equality operator that takes a type as an additional argument is usually absolute in the sense the type does not affect the truth value of the equality. We explore the design of formal systems where ternary equality may be relative and depend on the type. The most promising application of such systems is that it yields a more natural treatment of quotient types: if two objects can be different at the base type but equal at the quotient type, we can use the same representation in both types without having to use equivalence classes. The main drawback of such a system is that the substitution of equals by equals becomes more complex as it now depends on the type with which the objects are used. |

13:30 | ABSTRACT. Set theory has long been viewed as a foundation of mathematics, is pervasive in mathematical culture, and is explicitly used by much written mathematics. Because arrangements of sets can represent a vast multitude of mathematical objects, in most set theories every object is a set. This causes confusion and adds difficulties to formalising mathematics in set theory. We wish to have set theory's features while also having many mathematical objects not be sets. A - non-set ordered pairs,
- non-set natural numbers,
- a non-set exception object that can not be inside another object
- modular combinations of these features.
We show how to axiomatize GSTs and how to build models for GSTs in other GSTs. |

14:00 | A New Export of the Mizar Mathematical Library PRESENTER: Colin Rothgang ABSTRACT. The Mizar Mathematical Library is a prime target of library exports that make proof assistant libraries available to knowledge management or other deduction systems. The library has been exported multiple times in the past, including our own export from Mizar to OMDoc done in 2011. But the exporters tend to be very difficult to maintain. We present a complete reimplementation of our previous export. It incorporates many lessons learnt and improvements made both on the Mizar and the OMDoc side. |

14:15 | Gauss-lintel, an algorithm suite for chord diagrams exploration ABSTRACT. Gauss diagrams, or more generally chord diagrams are a well-established tool in the study of topology of knots and of planar curves. Not every Gauss diagram corresponds to a knot or a planar curve; if it does, it is called realizable. Many realizability criteria and decision algorithms have been proposed since the 1930s. Recent studies in 2018-2019 formulated especially simple conditions related to realizability which are expressible in terms of parity of chords intersections. In this paper we present system description of Gauss-lintel, an algorithm suite for chord diagram exploration, implemented in SWI-Prolog. Gauss-lintel utilizes a concept of "lintel", which is a list representation of an odd-even matching of the set of integers [0,...,2n-1], for efficient generation of Gauss diagrams satisfying various properties, including the variants of realizability conditions. We report on extensive experiments in generation and enumeration of various classes of Gauss diagrams, as well as on experimental (in)validation of published realizability conditions. |

Invited speaker

15:00 | Doing Number Theory in Weak Systems of Arithmetic |

Regular papers

Doctoral programme