Computational Logic


Roy Dyckhoff headed the research activity at St Andrews in computational logic. He is now (since 2011) retired, and thus is no longer inviting PhD applications; but continues as an active researcher, publishing articles and giving talks at workshops and conferences. His and his students' (and research colleagues') work included the development of proof assistants and theorem-provers for various logics, the exploitation of various logics for problem specification or as programming languages, and the investigation of their proof theory and semantics.


SImPL EC grant (April 2010 -- March 2012) (held by Vladimir Komendantsky). See also the Archive of papers

Computational Logic in Artificial Neural Networks EPSRC grant (Oct 2008 -- Sept 2011) (held by Ekaterina Komendantskaya)

Proof Theory and Constraint Satisfaction EPSRC grant (Jan--May 2008) for collaboration with James Caldwell and Ian Gent

Lexicalized Proof-Theoretic Semantics of Natural Language EPSRC grant (Feb--August 2007) for collaboration with Nissim Francez and James McKinna

Embounded: Automatic Resource Prediction for Embedded Systems Esprit Framework 6 grant (June 2005 -- Feb 2009) for collaboration with Kevin Hammond, Greg Michaelson, Martin Hofmann et al.

Logic Structures for Control EPSRC grant (2004--2007) for collaboration with Ursula Martin

Former Members

Andrew Adams, Marta Bilkova, Muffy Calder, James Caldwell, Peter Chapman, Hans van Ditmarsch, Nissim Francez, Paul Gerrard, Taher Tawfek Hamza, Jacob Howe, Ruth Hardy (now Ruth Letham), Ekaterina Komendantskaya, Vladimir Komendantsky, Jael Kriener, Stéphane Lengrand, Neil Leslie, Thomas Peillon, James McKinna, Luis Pinto, Robert Rothenberg, Christian Urban

Prof. Muffy Calder was, from March 2012 to December 2014, Chief Scientific Adviser for Scotland .

Research Collaboration and/or Hosts of Visits:


Susanne Bobzien (at Oxford)


James Caldwell (at Wyoming)
Agata Ciabattoni (at TU Wien)
Giovanna Corsi (at ISA Bologna)
Nissim Francez (at Technion, Haifa)
Gerhard Jäger (at IAM, University of Bern)
Delia Kesner (at Paris VII (PPS))
Ekaterina Komendantskaya (at Heriot-Watt, Edinburgh)
Kai-Uwe Kühnberger (at Osnabrück)
Stéphane Lengrand (at the École Polytechnique, France)
James McKinna (at Edinburgh)
Sara Negri (at Helsinki)
Luis Pinto (at Braga, Portugal)
Stephen Read, Arché Research Centre, St Andrews
Mehrnoosh Sadrzadeh (at QMUL)
Peter Schroeder-Heister (at Tübingen)
Helmut Schwichtenberg (at Munich)
Christian Urban (at KC London)
Computational Logic Network: "COLOGNET"
Proof Theory Group (Dresden University of Technology) (picture)
Dependable Continuous Mathematics for Critical Systems
NETCA (UK Computer Algebra Network)
Embounded project

Publications and Talks:

RD gave a Contributed Talk at the Workshop on Structures and Deduction (Oxford, September 8--9, 2017).

RD was an Invited Speaker at the Symposium on Modalities, Conditionals and Values (Celebration of the Centenary of Georg Henrik von Wright, Helsinki, Finland, 23--25 May 2016).

RD was an Invited Speaker at the Workshop on Efficient and Natural Proof Systems (Bath, UK, December 2015).

RD gave a Contributed Talk at the Conference on General Proof Theory (Tübingen, Germany, November 2015).

RD was an Invited Speaker at the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Wrocław, Poland, September 2015).

Publications; Talks.

Logic Software:

Click here


Valid HTML 4.01!