This paper introduces a new approach to automating the task of evaluating the algorithms used to match job applicants to companies or students to schools.

The development of algorithms to match, for instance, students to schools or organ donors to patients has been one of the grand success stories of the Economic Sciences, leading to significant benefits to society at large. This was recognised with the Nobel Prize awarded to Alvin Roth and Lloyd Shapley in 2012.

Ideally, we would like to design matching algorithms that satisfy a wide range of attractive properties, such as leading to stable assignments, being fair, or incentivising participants to be truthful. But understanding the precise limits of what is possible in this domain is very difficult and continues to be an active area of research in Economics.

In this paper, I describe a new approach to automate some of the tasks of researchers in Economics who investigate the possibility of designing a new matching algorithm with a given set of desirable properties. The basic idea is to encode these properties in a logical language, thereby reducing the question of whether a matching algorithm of the desired kind exists to the question of whether a certain (very large) formula is logically consistent.