HEDA 2023
co-located with STAF 2023
Thu 20 Jul 2023 13:30 - 14:30 at Willow - ICGT Session 7: Keynote & Journal-First Chair(s): Chris Poskitt

A formal proof is a proof within an axiomatic system, where proof steps are either applications of axioms or applications of formally proven statements. Formal proofs have a long history within mathematics, starting with Euclid’s element’s which had an axiomatic system for geometrical reasoning. The main motivation of constructing a formal proof is obtaining unambiguous detailed proofs that can be mechanically checked. The advent of computer-based tools for formal proof, such as automatic and interactive theorem provers, made it feasible to produce formal versions of proofs that would otherwise be impossible.

A matching in an undirected graph is a subset of the edges of the graph s.t. no two edges are incident on the same vertex. In addition to the rich mathematical structure exhibited by matchings, algorithms to compute matchings have many applications, ranging from matching kidney donors and recipients to the allocation of advertisers to users of search engines.

In this talk, after giving an overview of the state-of-the-art, I will discuss my work on applying formal proof technology to matching theory, discussing some interesting findings and the even more interesting open questions.

Slides (presentation.pdf)734KiB

Thu 20 Jul

Displayed time zone: London change

13:30 - 15:00
ICGT Session 7: Keynote & Journal-FirstICGT Journal-First / STAF Keynotes at Willow
Chair(s): Chris Poskitt Singapore Management University

Remote Participants: Zoom Link, YouTube Livestream

13:30
60m
Keynote
Formal Mathematics: Matching Algorithms as a Case Study
STAF Keynotes
Mohammad Abdulaziz Technische Universität München
File Attached
14:30
30m
Talk
Fast Rule-Based Graph Programs
ICGT Journal-First
DOI