Archive for the 'Logic' Category

Paraconsistent Logic

Monday, October 1st, 2007

View as: view on E2  view as PDF

In the classical logic typically applied to mathematics, a single contradiction is fatal, as it allows anything and everything - including its opposite- to be derived. However, real-world situations such as large software products often feature irresolvable conflicts, from which we would not wish to draw such broad conclusions. Reasoning about such systems motivates the study of paraconsistent logic. The linked article examines the various ways in which the explosion of inconsistency can arise, and thus which rules of inference need to be discarded for such logics.

My interest in this topic arises from a talk I recently attended by Carl Hewitt, and wading through two dozen short essays on Russell’s Paradox by my new students!

On logic

Thursday, May 24th, 2007

As part of my postgraduate life here in Edinburgh, I’m expected to tutor a couple of dozen first (of four) year undergraduate Mathematics students. Thus I was involved in the marking of their group theory exam last Friday. As the questions were being assigned to markers, there seemed to be a reluctance to take the logic question, probably because students manage to tie themselves in hard-to-follow knots with this material. However, I spent some of my previous year at Bath tutoring on set theory and logic to Physicists, so was prepared for the worst, and I’d also spotted that the question was multiple choice, so the actual marking shouldn’t be too taxing, so I took responsibility for that one.

Still, 207 scripts later I was somewhat worried by the general standard. There were quite a few attempts which received full marks, but many more received zero, including elsewhere high-scoring candidates. Whilst the emphasis of a group theory exam should be group theory, the pressure of an exam and lack of access to notes will always dampen performance, and I probably received a few scripts that were pure guesswork, that’s still a disappointment. Whilst it pains me to say it, a student could become competent at first year undergraduate mathematics just by learning how to ‘turn the handle’ of appropriate bits of mathematical machinery, and as this is pretty much all that they do at school, they may find that university-level mathematics isn’t really the subject they thought it was. To make the leap from computation to understanding, it strikes me as vital to gain mastery of basic logical manipulation. Nor should this just be the domain of Mathematicians; if anything, a precise understanding of the structure of an argument (and its falsification) should be even more crucial to the Humanities.

So I’m going to reproduce the question here and then attempt to unravel it in a precise manner but without recourse to the more abstract approaches of formal logic, in the hope that everyone can follow. Here goes:

Consider the statements:

A. All people who can sing in tune are musical.

B. Some people who cannot sing in tune are musical.

C. Some unmusical people can sing in tune.

D. Some unmusical people cannot sing in tune.

E. No unmusical person can sing in tune.

Mark with the number 1 any of the statements B,C,D,E that are logically equivalent to statement A, with 2 any that are (logically equivalent to) the negation of A, with 3 any that are (logically equivalent to) the converse of A, with 4 any that are (logically equivalent to) the negation of the converse of A and with 0 any which are in none of the above categories.

Solution is behind the cut, so if you want to try this yourself without spoilers, now’s the time!

Read the rest of this entry »

The Secrecy Problem

Thursday, May 3rd, 2007

I took a number of interesting modules in formal logic as an undergraduate, and I’m often fascinated by ideas in this field. There are natural connections between cryptographic protocol analysis and string rewriting, and with enough freedom one can emulate general models of computation such as Turing machines by protocols. One particularly neat side effect of this is that it allows an elegant proof of the undecidability of the secrecy problem: namely, given a protocol and a secret message, is there a decision procedure to establish whether an intruder can learn the secret? By reducing to Post’s Correspondence Problem, it can be shown that the answer is no! Of course, this raises issues of intruder strength and ‘honest’ protocols; I’ve written up some of these ideas (along with the proof and an outline of PCP) over on e2.

NP vs Co-NP

Saturday, May 13th, 2006

view as PDF

The NP vs co-NP problem is related to the more famous P vs NP question. As part of CM30071:Logic and its applications (University of Bath Computer Science), my group gave a presentation on this topic, and its connections to propostional logic (through the satisfiability and validity problems). The attached file contains a two page summary of the main ideas from the talk.

Infinite Descent

Friday, March 3rd, 2006

View as: view on E2  view as PDF

A version of proof by contradiction usually found in number theory.

Register Machine

Thursday, May 6th, 2004

View as: view on E2  view as PDF

From Turing machines to Register machines- overview, instruction set and simple examples. Simulation of recursive functions by Register machines (with proofs in macro form).

Clausal form

Tuesday, February 10th, 2004

View as: view on E2  view as PDF

A standard form for first order formulae that consists of a number of clauses (series of atoms in conjunction that imply a disjunction of atoms). Brief overview of clauses (such as the headed horn clause used in Prolog/Cyc); clausal form algorithm; a worked example.

Language recognition and generation in Prolog

Thursday, January 29th, 2004

View as: view on E2  view as PDF

A demonstration of weaknesses in Prolog’s goal-matching method in the context of language recognition/generation. Considers decidability, term languages, statement form, arbitrary strings from a restricted alphabet.

Prenex and Skolem normal forms

Tuesday, January 20th, 2004

View as: view on E2  view as PDF

Two standard forms for first order predicate logic- Prenex normal form requires all the quantifiers to be at the front, whilst Skolem form further demands that only universal (forall) quantifiers are used . Gives an algorithm for finding prenex form with worked example; consideration of Skolem functions; Skolem normal form algorithm; a consideration of logical equivalence and the merits of these normal forms.

Semantic Tableaux proof method for predicate logic

Friday, January 16th, 2004

View as: view on E2  view as PDF

A backward-chaining proof method for predicate logic, motivated by proof by contradiction rather than deduction. Description of the semantic tableau structure and rules, with suggested order of application. Also includes worked examples and a proof of correctness and completeness (with reference to Gödel’s theorems).