Notices

  • Help Session, Thursday July 2, 1pm-3pm, Room 204, K17 Building

    Posted by Sebastian Sequoiah-Grayson Wednesday 01 July 2026, 02:30:39 PM.

    Hi everyone,

    Help Session, Thursday July 2, 1pm-3pm, Room 204, K17 Building : )

    All best,

    Seb

  • Infinte trees

    Posted by Sebastian Sequoiah-Grayson Tuesday 30 June 2026, 03:43:20 PM.

    Hi everyone,

    A quick note on infinite trees and how to specifiy a countermodel.

    An infinite tree is one that forces us to add new constants via existential quantifier elimination during our attempt to saturate an open path. Here is an example (using `Ex' for the existential quantifier):

    Suppose that you have a tree with

    EyRay

    on an open branch, and you eliminate the existential quantifer getting

    Rab

    Suppose also that in an attempt to saturatrate this open path that you ended up with another instance of hte same existential quantifer, this time as follows:

    EyRby

    which you eliminate again, getting this time

    Rbc

    and so on and on....

    Even with only two iterations of exitential quantifier elimination, it is obvious that the next one will be

    EyRcy

    from which you will get

    Rcd

    and then Rde, and then Ref, Rfg, Rgh, Rhi....

    and so on infinitely.

    In this case the domain D of your countermodel will need infinitely many objects D : {1, 2, 3, 4, 5, 6, 7, 8, 9....}, and infinitely many names with the appropriate mappings to objects in D - a:1, b:2, c:3, d:4, e:5, f:6, g:7, h:8, I:9....

    Given the instances of R in the open path above, you can specify the extension of R as follows:

    R : { <1, 2>, <2, 3>, <3, 4>, <4, 5>....}

    And then you are done.

    Good luck with Assignment 2!

    All best,

    Seb

  • Thank you everyone : )

    Posted by Sebastian Sequoiah-Grayson Tuesday 30 June 2026, 03:30:37 PM.

    Dear denizens of COMP2111,

    Thank you so much for being awesome, and for making the very first iteration of the new version of COMP2111 so fantastic. You are the best! Thank you for your excellent questions, thank you for being so genuinely interested in the topic, and thank you for all of your hard work so far and for the rest of the term.

    Next stop...Vineet! I shall be there on Thursday also and I am looking very forward.

    All best,

    Seb

Upcoming Due Dates

There is nothing due!

Back to top

COMP2111 26T2 (Foundations of Formal Methods) is powered by WebCMS3
CRICOS Provider No. 00098G