The project envisioned in the proposal involved the student familiarising him- or herself with deontic logic and its extensions---chiefly temporal and dynamic deontic logic---and exploring in detail at least one practical application: taking some particular system arising in everyday life (self-driving cars, electronic contracts, etc.) and using the resources of deontic logic to completely formalise it, ideally with an automated verification of correctness of the axiomatisation. This is at least partially accomplished in the thesis at hand, which does indeed provide an introduction to deontic logic and its extensions, along with a very preliminary application of this language to the formalisation of ethical behaviour in AI systems.

The goal is an essential one: AI now makes critical decisions in almost all areas of life, including but not limited to health care, employment, law enforcement deployment patterns, targeting of military strikes, and criminal sentencing. The tool used, dynamic deontic temporal logic, is highly suitable, as it allows the formalisation of ethical norms, captures changes of obligations over time, and incorporates a calculus of actions and their consequences. Successfully executed, the project would likely have been suitable for publication, e.g. in the proceedings of a computer science conference. Sadly, as mentioned above, the execution is not entirely successful.

While the student is to be admired for undertaking a project which, given his light background in formal logic, would have required a determined and focused effort to learn and apply new ideas over the course of the year, he has been very heavily dependent on my input, and largely unable to independently remedy (or even detect) deficits in his own understanding through independent reading or posing clarifying questions.  As a result, I fear he has not acquired a truly deep understanding of the ideas present in the thesis. Without repeated intervention on my part, misunderstood concepts remained misunderstood, and without repeated pushing on my part, the thesis might have consisted of a jumbled collage of material taken from other sources, with little original, independent contribution.  It has been a long process arriving at the final result.

Still, the student has managed to do something of genuine interest: the only existing attempt at a formalisation of AI ethics, in the here oft-cited paper of Priya T.V. and Shrisha Rao, has a host of shortcomings, including an insufficiently formalised logical language, elementary errors in formal proofs, and axioms which clearly do not have the intended meanings.  The current thesis fixes these issues completely, giving a real first approximation of a system of axioms for ethical behaviour of a general AI system. Naturally, a more ambitious project would not simply correct these existing axioms, but assess their appropriateness, and consider substantially different possibilities, formally checking correctness of the resulting system. The Future Directions section suggests a way of pushing this approach further, capturing the meaning of ethical behaviour in particular AI systems by conditioning ethical requirements on particular sequences of actions intrinsic to each system. This, too, would have been interesting to pursue further, say in detail for some particular AI system, e.g. the COMPAS criminal justice system.

The result is a thesis which, in my view, represents a degree of effort and understanding that should be regarded as satisfactory: I therefore recommend a grade no lower than D, and feel that a D itself would not be unreasonably.  I note, though, that my assessment is based on the entire process of producing the thesis, and on my sense of the depth of knowledge behind it: it is possible that the finished product itself is deserving of a higher grade.  An argument could certainly be made for a C.  In that case, I defer to the opponent and the members of the committee.

Deontic logic, which is a variant of modal logic, provides a convenient mathematical framework for dealing with normative concepts like obligation, permission, and prohibition. The thesis is concerned with the ethical principles in the dynamic deontic linear time temporal logic (DDLTL). Its goal is to obtain effective mathematical tools for expressing, analyzing, and verifying ethical behavior of AI systems. 

The problems investigated are clearly formulated and the thesis scope is well defined. The author is apparently well conversant with the related literature listed in the comprehensive enough bibliography included. The material presented is organized in a clear, systematic and logical manner and the mathematical conclusions are correct. The overall linguistic, stylistic and technical editing of the thesis is very good, I found only a few minor misprints and one marginal inconsistency when the abbreviation DLTL is used for both the deontic linear temporal logic (p. 28) and the dynamic linear temporal logic (p. 33).

The main contribution of the thesis is a modification (correction) of axioms of DDLTL in order to eliminate some logical inaccuracies and redundancies and to better capture normative concepts for AI systems. But it is a deficiency that no implementation of the theoretical outcomes is presented because such an implementation would confirm the eligibility of the axioms modified for analyzing ethical behavior of AI systems. My question therefore is whether the author plans, as a future work, to deal with such implementations.

As a conclusion, I would like to express my opinion that the author has showed the ability to understand mathematical techniques and methods and organize a mathematical text. The overall quality of the thesis is very good and the topic is timely as AI systems are increasingly integrated in our everyday life and ethical problems connected with their use become a very important issue.