Geometrisation of first-order logic

Dr. Roy Dyckhoff will give a talk titled, “Geometrisation of first-order logic”.


We show that every first-order theory T has a conservative extension G_T that is a geometric theory. Reasoning problems in T can therefore be replaced by problems in G_T, where the methods of geometric (aka ‘coherent’) logic are applicable. We discuss related work by Skolem (1920), Antonius (1975), Bezem and Coquand (2005), Fisher (2007–..), Polonsky (2011) and Mints (2012).

(A formula is **positive** iff built from atoms using \exists, \land and \lor. A **geometric implication** is the universal quantification of a formula C -> D where C and D are positive. A theory is **geometric** iff axiomatised by geometric implications. Lots of mathematical theories are geometric. Reasoning in a geometric theory usually avoids the unnatural conversions of resolution-based theorem proving, and produces intuitionistically sound proofs)

Joint work with Sara Negri (Helsinki).

Event details

  • When: 21st February 2014 12:00 - 13:00
  • Where: Maths 1A Tut Rm
  • Format: Talk

Cybersecurity for Critical Infrastructure

Cybersecurity for Critical Infrastructure, or ‘how to break into a nuclear power station for fun & profit’

Dr Richard Gold, Cisco Systems, UK

Cyber Security for Critical Infrastructures such as the power grid, oil & gas pipelines and dams has become a hot topic since the Stuxnet malware attack against the nuclear enrichment centrifuges in Iran. However, due to intrinsic issues with the field of Critical Infrastructure (a.k.a., ICS or SCADA), it is difficult to deploy standard IT security solutions “as is” to these systems. In this talk I discuss the problems associated with deploying effective security processes in Critical Infrastructures, the various types of security holes which these system contain and a step-by-step approach to exploiting a Critical Infrastructure installation. Thinking from the attacker’s perspective allows us to get an insight into how these systems are vulnerable and how a potential attacker might exploit them.

Event details

  • When: 18th February 2014 14:00 - 15:00
  • Where: Maths Theatre B
  • Series: School Seminar Series
  • Format: Seminar

Intellectual Property – What, why, and how?

Dr Alan Boyd and Dr Nicholas Malden, D Young & Co LLP (Patent Attorneys)
Intellectual Property – What, why, and how?
In many technological fields, especially computer science, output isn’t a physical object that can be sold, but is an idea or an expression of an idea that comes from your mind. But how can industry take advantage of such ideas or expressions, and what’s to stop a competitor from simply copying your hard work and benefiting from it at your expense? In this talk, we’ll take you through the basics of Intellectual Property (IP) and look at how it can be used by a computer scientist, its importance to new start-ups and large multinationals alike, and also introduce you to the patent attorney profession. We’ll give you a chance to try your hand at writing a patent claim, and we’ll give a prize to the best one!

Event details

  • When: 5th November 2013 14:00 - 15:00
  • Where: Purdie Theatre C
  • Series: School Seminar Series
  • Format: Seminar

Lab PC upgrade

The School has started the tender process for replacement of our Lab PCs. The new PCs will have a similar form-factor to the current PCs but will have faster more power efficient CPUs, more memory, quieter cooling and twin HDDs for simpler dual boot configuration. We will be replacing the current displays with LED back-lit HD (1920×1080) screens and some of the PCs will have dual displays.

The current timetable will see the new PCs deployed in January.

Shuttle SH61R4 H61 PC base unit

Base unit for the new CS Lab PCs - Shuttle SH61R4 H61

The components specified in the tender are as follows:

  • Shuttle SH61R4 base-unit.
  • Intel Core i5, 3450S, 2.80GHZ, 65W CPU.
  • 8GB DDR3 1333MHz memory.
  • Dual 250GB HDD, 5400RPM, energy efficient.
  • 21” – 24”, 1920 x 1080, LED backlit, DVI, energy efficient display.