Computational Logic

Introduction

Roy Dyckhoff heads the research activity at St Andrews in computational logic. His and his students' work comprises 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. He retired in September 2011, and thus no longer inviting PhD applications; but he intends to continue as an active researcher. Juliana Bowles works on formal foundations of object-oriented specification languages in the context of large-scale distributed systems. Her main interests include true-concurrent logics for describing dynamic aspects of large distributed object systems, logics of knowledge and belief, and applications of category theory. Ian Gent works on search algorithms, experimental methods in CS and AI and constraint satisfaction problems. Vladmir Komendantsky works on the representation of extended regular expression languages using dependent type theory and the formal verification of properties of functions manipulating such languages.

Local Seminars

Grants

SImPL EC grant (April 2010 -- March 2012) (held by Vladimir Komendantsky)

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

Local Members

Juliana Bowles, Edwin Brady, Roy Dyckhoff, Ian Gent, Vladimir Komendantsky

Non-local Members and ex-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, Ekaterina Komendantskaya, Jael Kriener, Stéphane Lengrand, Neil Leslie, Thomas Peillon, James McKinna, Luis Pinto, Robert Rothenberg, Christian Urban

Research Collaboration:

Current:

Old:

Publications and Talks:

Publications; Talks.

Events:

ARW 2012 (Manchester)

Logic Software:

Click here

Links:

• Automated Reasoning Workshop
• Michel Levy's theorem provers
• IEEE Symposium on Logic in Computer Science
• ACM Transactions on Computational Logic
• International Masters programme in Computational Logic

Links2Go Logic