Dr Alexander Bolotov

In short - my background is in mathematical logic, proof theory and philosophy. I gained MSci in Logic (1985), and first PhD, in Logic (1992) both from the Lomonosov Moscow University. My second PhD (2000), in Computer Science was from the Manchester Metropolitan University. I studied clausal resolution technique for branching-time logics. I was a postdoc at MMU until 2001, when I moved to Westminster as a Senior Lecturer in AI. I am now a Reader and a co-lead of the Westminster AI Network.

A little longer story of my academic journey is here. 

My background is in mathematical logic, proof theory and philosophy. I gained MSci in Logic (1985), and first PhD, in Logic (1992) both from the Lomonosov Moscow University. My supervisor, Professor Voishvillo was my mentor in life. With his honesty and genuine scientific nature, he was a  perfect example of somebody who was not comfortable with any type of faking, in science or life. 1991 and 1992 where two transformation years which brought me closer to computer science. I printed my first PhD in a computer lab, which I led; the lab was full of bulky slow computers without hard disks. I used ChiWriter - one of the first word processors supporting maths typing. While I was printing my dissertation on proof search in relevant logic, all lab’s printers, one by one, died. In parallel, together with Vyacheslav Bocharov, Professor of Logic and my former teacher, we developed a proof search procedure for natural deduction calculus for propositional, and later a semi-automated proof search for first order natural deduction. This has been the starting point of my passion to this form of reasoning. The proof search was implemented by my first programming teacher and a good friend, Alexander Gorchakov who brought me closer to computing in general. Relevant logic brought me the next stage in my career - I was absolutely lucky to spent a year with Nuel Belnap, Alan Ross Anderson Professor at the University of Pittsburgh (USA). This visit and Nuel himself were two massive subjects dramatically changing my career and life. While based in Pittsburgh, with Nuel's suggestions, I had a privilege to meet a number of great logicians. Wearing shorts and with an old backpack I was unexpectedly delivered by a huge luxury limo from Indianapolis airport to spend time with Mike Dunn and his research group at the Indiana University. In Prinston University I met John Burgess. An exciting visit to Daniel Dennett at MIT where he showed me a one leg robot rolling over the lab - and this was just shocking in 1994. I was part of extra curriculum seminar on type theory lead by Peter Andrews, at Carnegie Mellon University. All these visits formed my strong interest to theoretical computer science and AI, proof search, modelling and algorithms. Based on these I started looking for a PhD openings, applied for one in Manchester, under the supervision of Michael Fisher, and subsequently moved to Manchester. That PhD programme, on the development of Clausal Resolution Technique for Branching-Time Logic, was absolutely unforgettable experience. It brought me deep understanding of new topics such as complexity, automata, or fixpoint calculi. It also brought me fantastic co-authors - Michael Fisher andClare DIxon. It brought me invaluable experience of Fisher's research group and of its members, one of them was Mike Wooldridge, who does not need any introduction for practically any researcher in theoretical CS or AI. Colin Stirling at Edinburgh hosted my research visit and played the crucial role in finding an interesting and winning strategy for the formulation of sound and complete resolution procedure for CTL. Looking for the external examiner for PhD Michael Fisher suggested Dov Gabbay saying that Gabbay as the external means - he would either like your work in which way a pass is guaranteed or completely completely dislike it. That looked good to me. When the viva just started, Dov said - "you passed, now we cant start the viva". My postdoc at Manchester Metropolitan University was devoted to the study of the extension of clausal resolution to mu-calculus. With this background, in 2001, Westminster attracted me with Senior Lectureship position in AI and I am still here, at Westminster.

I co-lead a university-wide AI research Centre - The Westminster AI Network with over 100 AI researchers from every Westminster school. 

My core research has been in the area of formal specification and verification, where I published over 80 papers developing proof based verification methods. In particular, I am interested in the application of labelled deductive systems to verification of dynamic systems. I have developed a clausal resolution method for branching-time logic CTL and its extensions: ECTL and ECTL+ (supervising a PhD of Artie Basukoski), the systems that allow to express more complex properties of reactive systems. I am collaborating with Lorea research group at the University of Basque Country on the development on one-pass tableaux verification techniques, and, in particular, on developing proofs with certificates.    

My other area of interests is graph-based reasoning. I supervised a PhD of Natalia Yerashenia, which built a generic architecture of ML Predictive Models based on graph-based reasoning.   

More recently I became interested in the Specification and Verification of AI system, and more specifically in assuring the security of AI applicaitons. My collaborators in this area are Natalia Yerashenia, Ayman Al Hajjar,  Ayman Al-Hajjar, and Tom Oliver.

My Erdos number is four and my Dijkstra number (a similar calculation of the co-authorships paths leading to Dijkstra) is also 4.  

For details of all my research outputs, visit my WestminsterResearch profile.