Work Journal August 28-September 1 I've mostly been working on the final paper this week. I've had a meeting with Professor Ternovska about it and I've got a pretty good idea of what I'm writing (and have written). I've had a great term this summer and I'm really looking forward to going to Banff with my father (who is flying out to Vancouver next week). I'm also really looking forward to the start of my third year!

August 21-25 Professor Ternovska came back from Seattle this week! Professor Mitchell's student won the student SAT solver competition at FLoC and Mirek Truszczynski (one of the founders of ASP) said that MX is the right way to go for declarative problem solving! Also, Marc Denecker and his PhD students are visiting Simon Fraser University so we're holding workshops with them all this week to discuss the project both groups are working on (such as ironing out some simple input syntax differences, method for efficient grounding, and things to work on in the future, i.e. functions and arithmetic).

August 14-18 I've begun the process of writing up my final paper for this summer's research project. I've made a list of things to include and hopefully I'll be able to discuss more of this with Professor Ternovska when she gets back from Seattle. I've also put the n-queens example into the input syntax for testing. Later Raheleh told me there was a mistake with the axiomatization that Faraz had written so I made the appropriate changes in the library as well.

August 7-11 This week Professor Ternovska, Professor Mitchell, Yongmei, and Murray left for Seattle for the FLoC conference, where they will be presenting a paper and organizing the LaSH workshop. They left on wednesday so we still had our weekly project meeting. I have finished the n-queens example, and hopefully I will be able to help Raheleh these next few weeks.

July 31-August 4 After this week's project meeting, I made a few changes to the library such as specifying that some of the functions are now built-in, including a date on the document, explained the expansion predicates more indepth, and set a standard way of writing out multi-sorted universes (since different papers had different methods for this). During the meeting, the MXP group was trying to come up with an axiomatization for n-queens, which turned out to be quite a bit more difficult than I thought it would be due to the fact that we cannot use arithmetic. Previously, we had a similar problem while working on an n by n sized Sudoku grid, but we avoided it by fixing the board size to 9 by 9. However, we cannot do the same for this problem. I also added Faraz's Bounded Model Checking example to the library this week. It is quite long, I'm not sure if it is going to stay in the library.

July 24-28 This week I attended the weekly project meeting and another meeting with Professor Mitchell, Faraz, and Raheleh. In both meeting we went over the benchmark problems done by other groups that we want to axiomatize and test so we can compare the results with the other groups'. We came up with new axiomatizations for graph colourability and sudoku (with a few variations). I think the next problem we want to include in the library is the n-queens problem. Professor Mitchell also brought in a few papers for the group to read. We're going to search for their examples and hopefully come up with our own axioms to test and compare results.

July 17-21 I finished adding the references to the examples that I've taken from other papers for the bibliography of the library. I also added alternative axiomatizations for several problems after the project meeting, such as Hamiltonian cycle and Graph Colourability. At the meeting I also presented the Circuit Fault Diagnosis done by Marc Denecker's group to the MXP group. I made a few mistakes in explaining the problem, but everything went smoothly. At the same meeting, Professor Mitchell suggested other problems to axiomatize, such as the popular logic puzzle Sudoku. I found a SAT paper by Ines Lynce about this topic which I've finished reading. I hope to have added this example to the library by the beginning of next week. On thursday's weekly logic seminar, Faraz gave a talk about his recent research work, which is bounded model checking as model expansion. I also hope to have this example added to the library by the end of next week.

July 10-14 Professor Ternovska and Professor Mitchell came back from Cambridge this week and we had a project meeting with both of them where we all discussed what we all have been doing for the past 3 weeks. I finished one of the planning problems and started trying to work out the bibliography for the problems I currently have in the library that I have taken from other research papers after Professor Ternovska suggested that I do so. I also added the hamiltonian cycle problem and another axiomatization for 3-colourability. At the project meeting on tuesday, Professor Mitchell described the different portions of the model expansion project and outlined what had already been done and what still needs to be done. Since we need to start more rigorous testing, I need to add more axiomatizations for each of the problems to test which will work better with the grounder and SAT solver.

July 3-7 Since monday was Canada Day, I spent the day with my uncle and his family and friends barbequing, which was lots of fun. On tuesday, wednesday, and thursday, I attended 3 complexity and computability seminars given by Dimitrios Thilikos, Seffi Naor, and Evgeny Skvortsov, respectively. I also decided on the axiomatization to use for the Haplotype problem and am still looking at the planning as model expansion problem. At the project meeting on tuesday, I talked to Yongmei and Raheleh about the library and I sent a working copy of the library to Yongmei so she could give me some suggestions. Raheleh also helped me by giving me some of her classnotes from a previous course she had taken.

June 26-30 This week I finished reading the Haplotype Inference paper and started working on the axiomatization. I have also started to read the Planning as MX papers that Professor Mitchell gave me before he and Professor Ternovska left for the conference and workshop in Cambridge. I found the planning papers to be quite confusing, I'll probably need the help of Yongmei or Raheleh later on.

June 19-23 On monday I attended a applied math seminar "Packing Discs in the Plane" given by Dr. Ronald Graham. It was quite an entertaining talk about how many non-overlapping discs can be placed into a square (or another shape). Thursday was another day filled with seminars since it was the IRMACS Discrete Math day at SFU. There was a whole roster of distinguished speakers talking about their research. This week I have put in some more problems into the MX library. I also started reading a paper titled "Efficient Haplotype Inference with Boolean Satisfiability". This is the first computational biology paper I've read and I found it quite challenging and interesting. It has taken me quite a bit of time to read.

June 12-16 This week I started compiling all the already axiomatized problems (from past model expansion papers) into one library using LaTeX. Since I have never used LaTeX before, I spent the beginning of the week learning how to use the language; the different formats and special commands for different symbols. I've wanted to learn to use it before, but this was a good opportunity to begin. So far it seems to an extremely useful tool. I attended a project meeting this tuesday along with a logic seminar given by Dr. Jamal Bentahar on thursday. The seminar's topic was Specification and Verification of Agent Communication in Multi-Agent Systems. Besides learning to use LaTeX, I have been looking at some other problems not yet axiomatized in other papers so I may include them in the library I am working on. Hopefully I will be able to work on some of these with the help of Antonina and Yongmei while Professor Ternovska is away in Cambridge.

June 5-9 I have been reading the proof of Fagin's theorem and Cook's theorem this week. It was slighly confusing the first time i read it since it uses turing machines to aid in the proof of Fagin's theorm. However, I later read the section on Turing machines in "Introduction to the Theory of Computation". I have also started compiling search problems for the library I will be creating as part of my first project. I'll be learning to create LaTeX documents next week.

May 29-June 2 This week I spent time learning about finite model theory. Both books I am reading on the topic are very interesting. "Finite Model Theory" by Ebbinghaus and Flum is more of a graduate-level book while "Elements of Finite Model Theory" by Libkin is slightly easier to understand. Professor Libkin is actually a Professor at the University of Toronto and the book was written for a graduate course which he teaches. I also noticed that he thanked Antonina Kolokolova in the book, a PostDoc (who is working with Professor Ternovska in the CL lab) I met this week and had read about previously from a link on Stephen Cook's webpage. I had a meeting with Professor Ternovska on tuesday about the project that I will be working on. The first project that I will be working on is creating a library of axoimatized NP complete problems. It will be useful when the group is testing their grounder and solvers for the model expansion project. The second project I will be working on later into the term will be related to Fagin's theorem. I am not entirely sure what the second project entails yet, but I will post more details when I find out. On thursday there was a project meeting which outlined the parts of the model expansion project, and also a seminar on spectra, both of which I attended.

May 22-26 Here is a copy of the research paper I had been talking about. It is written by Professor Eugenia Ternovska with Professor David Mitchell. On tuesday I met Moeen Karimifar, another undergraduate student who will be working with Professor Ternovska. I have been spending more time learning about first order logic, first order logic with inductive definitions, second order logic, semantics, and models and structures from "A Mathematical Introduction to Logic" by Enderton. I have also been reading more about complexity classes such as P, NP, and NPC from "Introduction to Algorithms" by CLRS, a textbook I have previously used for an algorithms course.

May 15-19 Most of this week was spent on reading and understanding the research papers I was given the previous week. Earlier in the week, I received my access card for the Computational Logic Lab. Also, Professor Eugenia Ternovska came back from her workshop and we met for the first time on friday. Because I didn't feel I fully understood the papers, she lent me some slides and books to study.

May 8-12 I arrived in British Columbia this week and I'm only beginning to get the feel of things around the area. I checked into McTaggart-Cowan Hall (which is a on-campus residence building) and met some of the other students staying on my floor. I also received some of Professor Eugenia Ternovska's research papers to read from her PostDoc Yongmei (who also showed me around campus and introduced me to some of the graduate students at SFU). It happens that both Yongmei and Professor Ternovska got their PhD's from University of Toronto!