Hi everyone,
Help Session, Thursday July 2, 1pm-3pm, Room 204, K17 Building : )
All best,
Seb
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
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
Hi everyone! An urgent request with regard to ACS acfredition. If any of you are on campus and freee today at 2pm, and if you are doing either CS, Advanced CS, or any doubble degree with CS or Advanced CS, then please do come to Room 113 in K17 for a quick and fun Q& A.
Many many thanks!!
Greetings everyone! Today is Engineering Australia accreditation day (Tuesday was ACS). I am on a panel from 10-11. I should be on time for the lecture but if I am a little late then this is why. The tutors will do a little dance to keep you entertained :
Greetings everyone! Today is Engineering Australia accreditation day (Tuesday was ACS). I am on a panel from 10-11. I should be on time for the lecture but if I am a little late then this is why. The tutors will do a little dance to keep you entertained :
Good morning everyone,
The first of your four assignements for COMP2111 is now available on webcms, under <Assignment 1> on the side-bar menu.
All best,
Seb
Hi 2111ers - I am send you htis on behalf of research colleagues at RMIT. Please do consider as they need your help : )
Dear Students,
You are invited to take part in a three-wave survey study as part of a research project (“Careers of STEM Students: Key Foundations and Empirical Examples in Defence”; human ethics approved by RMIT University – Project ID 27852). This study is conducted by researchers from RMIT University and Adelaide University (Professor Joe Jiang, Associate Professor Haiying Kang, and Associate Professor March To).
This project investigates the career interests, exploration, and choices of students studying science, technology, engineering, and mathematics (STEM) in Australian Universities. The findings will generate practical insights to support STEM students’ career planning and development, enabling more effective navigation of future job markets, while informing improvements in recruitment and selection practices of relevant sectors to enhance the experience of STEM talent.
If you are an Australian domestic student aged 18 or over, currently enrolled in a degree in science, technology, engineering, or mathematics, and interested in participating, please proceed to complete the survey below. Participation is entirely voluntary.
The current survey is Wave 1 and will take about 15 minutes to complete (actual time may vary, while Waves 2 and 3 will be much shorter). To thank you for your time, prize draws will be conducted for each wave. For Wave 1, the first 100 participants who provide valid responses will receive a $15 gift card . All other participants who submit a valid Wave 1 survey will be entered into a prize draw, with multiple gift cards available and a strong chance of winning.
You can access the survey here: <u>https://rmit.au1.qualtrics.com/jfe/form/SV_6V8phEDFKMx3gdU</u>
If you have any queries, please contact the research team. You are also more than welcome to share this project within your networks!
Research Team Members:
Professor Joe Jiang: <u>joe.jiang@rmit.edu.au</u>
Associate Professor Haiying Kang: <u>haiying.kang@adelaide.edu.au</u>
Associate Professor March To: <u>march.to@rmit.edu.au</u>
Good mornimg everyone : )
Yesterday's lecture recordings + this weeks tutrial qs + and updated version of the lecture notes are not on webcms (and moodle).
See you tomorrow!
Seb
Hi everyone,
I have uploaded today's lecture video to Moodle. It is on the main page, not under "Lecture Recordings".
Alas poor WebCMS is still on the blink!
Thanks for allof your great questions in the lecture today : )
See you on Thursday for more adventures in syntax,
Seb
Hi everyone! Webcms is playing up a bit so I have added the latest version of hte lecture notes plus this weeks tute Qs to moodle. Sorry I know that moodle is yuk but ti is a good work around for now. Gosh I hope this message gets through!!
This week we are covering the material in Part III.7 of the Lecture Notes - Syntax of Predicate Logic.
See you tomorrow : )
Seb
Hi everyone - as per the subject header : )
Hi : )
Just ftr - if you are enrolled in the online lecture stream you are of course still very welcome to attend in-person.
'til soon,
Seb
Hi everyone. Today's lecture video is now available on webcms under Lectures. I am exporting a colour-graded and audio-improved version from Davinci as I write this, but it takes hours to process. I shall upload it in the morning.
(As predicted, the Echo 360 video is a disaster. Sorry. But it is funny to watch. The one on webcms is from my phone.)
Most importnatly, thank you for all of your great questions today!!
Hi everyone : ) I have added some tutorial practice exercises for this week to webcms under Course Work. The idea is to have a read and a think and then you will work through them together in your tutorial with your tutor. It does not matter too much if you cannot get to them before the tutorial.
The practices exercises DO NOT count towards your final mark in any way. They are just there to help you build up your skill sets with regard to creating and running your own verification environments. We start small, but some of them for Week 1 are deceptively tricky nonetheless. Have fun, and see you today at 11!
With big thanks to Maxim Burykin for spotting two errors (the ommision of the base case in the inductive deifnintion of wffs, and an erroneous transformation of ~B into ~A in a tree-proof), the corrected lecture notes have been uploaded.
There wll be more typos I promise : ) If you think that you have spotted one then please do post in the forum and I shall hop on to it.
Thaks again Maxim, and see you all tomorrow for our first lecture!
Seb
Hi everyone!
I am writing a book for you: Formal Reasoning: A Guide for Humans and Machines : )
I have added a draft to webcms under <Lecture Notes>. I have added a Readings column to the Course Schedule section in the Course Outline.
Truth be told, you can probably make it through the course without reading the readings (I can hear you cheering as I write this), but they are there to cover everything in detial.
We are going to learn everything together by doing it together.
See you soon!
Seb
Aaaaaannnnnnnnd…let’s go!
Welcome to the brand new COMP2111 - Foundations of Formal Methods : )
Vineet and I are terribly excited about the whole thing really.
You can find the course outline on webcms here:
https://webcms3.cse.unsw.edu.au/COMP2111/26T2/outline
Please do read the course outline. It has a lot of information in it with regard to due dates for assessments and other things. But due dates are terribly boring I know. Content however, is not!
The first half of the course moves from propositional logic through to the Curry-Howard correspondence, via predicate logic, model theory, and intuitionistic/constructive logic. I know that some of you will be familiar with some of this whilst some of you will barely recall anythign from discrete maths. This does not matter. By the end of Week 2 everyone will be on the same page. I have done this before. Trust me : )
The second half of the course will take you through all things formal methods, via Dafny. The point here is that by the time we get to Dafny and verification and functional programming and whatnot, you will understand why it all works the way that it it does, not only how. This matters.
Vineet and I shall be giving the lectures. Edward is your course admin. Charran, Thomas, and Adam are your tutors.
To preempt - you have four assignments and they are take-home. The exam is in labs. Again, all dates are in the course outline on webcms that you will of course be reading carefully. Right? Good.
I shall be uploading lecture notes to webcms as they are ready. I am writing them as we go, which is exciting.
Is there anythign else? I do not think so. At least not yet. Oh yes, please come to the lectures in person. It is more fun and you will learn more. There will be a lot of board work.
Please do say hi below. Please do check the forum often. Please do help each other.
All best,
Seb