Read below or Subscribe to RSS feed RSS feed
  • Marks released

    Some marks are released. Check it on the Student Listing page. You will need your MACID and Student Number in order to login. Please note that empty records denote not available information. If you have any questions/corrections please contact the TA immediately.

  • Remainder about final exam: Dr Bruha explained during lectures what will be covered in final exam.

    Final exam will cover: topics covered during midterm I, II (syntax and semantic models of both propositional calculus & predicate calculus. syntax and semantic proofs. conversion into CNF, DNF. conversion into clause forms. resolution principle). program verification (you will be given small pieces of code and asked to prove pre/post-conditions, invariants and partial/total correctness). Temporal logic. convert English statements into LTL formulas. Semantics of LTL (given a state diagram model of LTL, prove/disprove the model satisfies some LTL formulas). In short, everything in the lectures/tutorials. You will find it in course slides I, II and in the sections Dr Bruha discussed from chapters 3 & 4 of the textbook. Good luck.

  • Midterm test 2 is marked out of 45. You can pick your test from the TA either during the tutorial or the office hour.

  • Sample solution for Midterm test 2

    Sample solution for Midterm test 2 is posted on the website. Check the course slides page.

  • Midterm test 1 is marked out of 35. You can pick your test from the TA either during the tutorial or the office hour.

  • On 28.Oct.2008, it was announced in the class that midterm test 2 will be held on 13.Nov.2008. It will cover predicate calculus including resolution principle.

  • 31 Oct 2008 Elaboration for problems on midterm I

    Problem 3 Syntactically (p v p) is equivalent to (p), (p v p), (not not p) and (p & p) but not (not p & p). But semanticlly it could be also equivalent to (not p & p). E.g. if p is F then (p v p) is F and (not p & p) is F also. In short, syntactically equivalent means: equivalent regardless of the valuation (semanticss).

    Problem 8 marks weight 10 divided: 4 for the truth table; 3 for CNF; 3 for DNF

  • 31 Oct 2008 Midterm 2

    test will cover: predicate calculus & resolution principle. definitions. transform a formula into clause form. prove using resolution principle. semantic systems of predicate calculus.

  • 30 Oct 2008 Midterm 1 Solutions

    I posted solutions on the website. Check the course slides page.

  • 28 Oct 2008 Midterm 2 remainder

    As already discussed and scheduled during lectures, you will have midterm test 2 on Thu 13 Nov 2008 during the class.

  • 27 Oct 2008: No TA office hours this week (27-31 Oct 2008)

    TA office hours for this week (on Wed 29 Oct 2008) are cancelled. Appointments could be made by email.

  • 23 Oct 2008: Midterm Announcement

    Midterm will be held on Monday 27 October 2008 during the class.
    You are supposed to know the material covered in lectures and tutorials and handwritten+typewrited set of slides.
    It will cover syntax and semantic systems and propositional calculus.
    No predicate calculus.
    You do not have to memorize any axioms or lemmas. We will provide you with all needed lemmas.
    Exam will consist of about 7 (generalized) multiple choice and about 4 writing questions.

  • No previous announcements