Logic and Applications Coursework Catch-Up

The lecturers and demonstrators for the Logic and Applications course held a ‘coursework catch-up’ today, the idea being that we can see where we went wrong in the assessed coursework pieces we submitted.

I think a big thank-you is warranted to the demonstrators on the course, Adam and Mohammad. These guys have been really helpful over e-mail as I’ve been doing the coursework pieces at home. It’s a little tricky because they can’t answer questions that are too open, nor can they confirm whether an answer is right or wrong. What seems to have worked this time is asking whether a coursework answer suggests that I’ve understood a specific concept.

I could have understood it and still made some small error and so got the answer wrong, so there’s no big reveal about what the answer is. The couple of times where there was a problem with my understanding, the demonstrators could just suggest that I review the relevant concept. Lots of thanks to those guys anyway for their patience and help!

After reviewing my marked coursework, I found that where I’ve lost marks it’s because of nothing more serious than typos which is nice to know. Now the revision process starts and there’s plenty to chew on with this one!


Logic and Applications Day 5

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.