So I’ve finished the Logic and Applications module now – the last coursework has been submitted and I’ve been enjoying a couple of days of doing things other than schoolwork!
The course was very focused on satisfiability – given a set of logical statements, is it possible to find an interpretation, a set of assignments for the logical statements, that satisfies them? That might not sound particularly useful, but it’s easy to express a question about a system this way.
As an example, consider the Minesweeper game. (Sorry if you’ve not come across this game before, check out the Wikipedia page for an example if so) Initially, we know very little and what we do know isn’t directly useful – how many squares there are. Once we’ve tried a couple of random clicks, we have some information we can use and express in these logics.
Perhaps we know that the square at 7 across and 12 up contains a mine and that the square at 8 across and 12 up has one adjacent mine. The question we might ask is whether 8,12 contains a mine and this is where satisfiability comes into play. Given logical statements encoding the rules of minesweeper, and the two details we mentioned specific to this game, is it possible that 8,12 contains a mine?
In other words, is the set of logical statements describing the rules, this game (to this point) and a statement expressing that 8,12 contains a mine satisfiable? The answer of course is easy for human to figure out.
The ability to automate the search for satisfiability allows these kinds of problems to be solved quickly and accurately using tried and tested reasoning tools. The general approach we used on the course was to search for a satisfying interpretation, which quickly leads to a problem – combinatorial explosion. The number of possible interpretations of a set of logical statements grows exponentially as the number of logical variables grows.
As such, a big focus on the course was algorithms and approaches to battle this exponential complexity – there are many techniques to reduce the space of possible interpretations and bring the complexity problem under control. That said, one of the impressions I come away with is that for a given problem no generalized technique will be able to guarantee to determine satisfiability in a reasonable time.
A final point, and an important one, is that the techniques we used were based almost entirely on mathematical proofs, that is to say that we are able to deduce that the techniques are correct and have certain other properties using formal methods. Of course, mathematical proof is formed by logical deduction too, so there’s a certain recursive nature to all this.
It’ll be good to get started on a fairly relaxed process of revision for all this stuff. The sheer volume of information thrown at us on these modules is huge, and it always feels a little like riding a rollercoaster, so it’s good to get back in there and review the material at a more relaxed pace.
crossedstreams.com 