The last couple of weeks have been quite hot in Toronto (mostly around 25 degrees C). I actually heard that this is unusually hot for September in Toronto. The humidity just makes it worse. You'll find yourself taking a shower three to four times per day.
Since last night, Toronto's temperature has cooled off quite a bit. Throughout today it's been around 18 degree C, just the perfect temperature. I wish it would be like this all year round. But that was just wishful thinking, because I have to be prepared for -20 degrees C in December and January. Actually somebody told me that during winter in Toronto, the wind can be quite strong. This will just make it worse ...
Friday, September 23, 2005
Favorite Logic of September 2005: First-order logic (1)
next
Some time ago I promised to make a series of postings on "My Favourite Logic of The Month" every month starting from September 2005. Well, here we officially start until we run out of "nice" logics.
Why first-order logic (FO)? It is the simplest non-trivial logic that we can use to express many mathematical statements. In fact, it is believed that first-order set theory is sufficient to axiomatize mathematics. Besides, most of you have already been exposed to FO, which will make my task much simpler. If any terminologies here sound obscure, check out preliminaries.
We will take a look at three aspects of FO: (1) the problem of testing satisfiability and finite satisfiability, (2) model-checking, and (3) expressive power. I am trying to cover topics that hopefully satisfy finite model theorists, and other logicians. In this posting, I will only speak about (1), saving the other two for some time next week.
Satisfiability: given an FO formula, test whether it is satisfiable. Well, what can we say about this problem with respect to FO? It is undecidable (actually r.e.-complete) [correction: complete for co-r.e, thanks to Richard Zach.]; this is a well-known result proven by Turing, which shattered Hilbert's dream to axiomatize mathematics. If you're into this kind of problem, check out the following book
The Classical Decision Problem by Grädel et al.
Actually, many fragments of FO are decidable, but most are provably intractable. The most complicated such result that I know of is Rabin's result of the decidability of monadic second order theory of infinite binary tree. [Whatever this means, but we may want to delve into this awesome result in the near future.] Although decidable, the problem has non-elementary complexity.
Finite Satisfiability: given an FO formula, test whether it has a finite model. I believe that this problem, if decidable, has more practical applications, e.g., databases. Unfortunately, this problem is also undecidable (actually complete for co-r.e.) [correction: complete for r.e.]. This result is due to Trakhtenbrot. Combining this result and that satisfiability is complete for co-r.e., we can readily imply that completeness theorem, which says that satisfiability is r.e. [correction: satisfiability is co-r.e., thanks to Richard Zach.], fails in the finite. Trakhtenbrot's result in fact marks the beginning of finite model theory. Later on, Fagin proved a logical characterization of NP with a technique that is "isomorphic" to that used to prove Trakhtenbrot's theorem (see this page). For more on finite satisfiability of FO, see Libkin's Elements of Finite Model Theory.
Some time ago I promised to make a series of postings on "My Favourite Logic of The Month" every month starting from September 2005. Well, here we officially start until we run out of "nice" logics.
Why first-order logic (FO)? It is the simplest non-trivial logic that we can use to express many mathematical statements. In fact, it is believed that first-order set theory is sufficient to axiomatize mathematics. Besides, most of you have already been exposed to FO, which will make my task much simpler. If any terminologies here sound obscure, check out preliminaries.
We will take a look at three aspects of FO: (1) the problem of testing satisfiability and finite satisfiability, (2) model-checking, and (3) expressive power. I am trying to cover topics that hopefully satisfy finite model theorists, and other logicians. In this posting, I will only speak about (1), saving the other two for some time next week.
Satisfiability: given an FO formula, test whether it is satisfiable. Well, what can we say about this problem with respect to FO? It is undecidable (actually r.e.-complete) [correction: complete for co-r.e, thanks to Richard Zach.]; this is a well-known result proven by Turing, which shattered Hilbert's dream to axiomatize mathematics. If you're into this kind of problem, check out the following book
The Classical Decision Problem by Grädel et al.
Actually, many fragments of FO are decidable, but most are provably intractable. The most complicated such result that I know of is Rabin's result of the decidability of monadic second order theory of infinite binary tree. [Whatever this means, but we may want to delve into this awesome result in the near future.] Although decidable, the problem has non-elementary complexity.
Finite Satisfiability: given an FO formula, test whether it has a finite model. I believe that this problem, if decidable, has more practical applications, e.g., databases. Unfortunately, this problem is also undecidable (actually complete for co-r.e.) [correction: complete for r.e.]. This result is due to Trakhtenbrot. Combining this result and that satisfiability is complete for co-r.e., we can readily imply that completeness theorem, which says that satisfiability is r.e. [correction: satisfiability is co-r.e., thanks to Richard Zach.], fails in the finite. Trakhtenbrot's result in fact marks the beginning of finite model theory. Later on, Fagin proved a logical characterization of NP with a technique that is "isomorphic" to that used to prove Trakhtenbrot's theorem (see this page). For more on finite satisfiability of FO, see Libkin's Elements of Finite Model Theory.
Thursday, September 08, 2005
CAPTCHA
It stands for Completely Automated Public Turing Test to Tell Computers and Humans Apart. Although I still wonder why it is abbreviated CAPTCHA instead of CAPTTTCHA, it was (re)brought to my attention due to the spam I got for my posting yesterday. Anyway, CAPTCHA is developed by researchers from Carnegie Mellon University. Here is their main website. Briefly, the goal of CAPTCHA project is to use Artificial Intelligence to help internet security (e.g. to prevent spams). The underlying assumption behind CAPTCHA is that there are tasks that humans can do, but computers can't. For example, since I enabled the word verification (from CAPTCHA project), each time you wish leave a comment on this blog, you will be asked to read and verify a distorted text (which is an image file). Although the task seems trivial to humans, tasks like this are non-trivial for computers (at least for now). We don't know whether computers will someday possess our ''intelligence''. But CAPTCHA is one reason why a 'no' answer will have positive impact on our society.
Ironically, the distorted texts are actually generated by computers ...
Ironically, the distorted texts are actually generated by computers ...
Wednesday, September 07, 2005
Back!
Hello all! It's been quite some time since I blogged last. But I am happy to inform you that I can start blogging again on a regular basis.
A little bit about my summer internship in Los Alamos ... I'll start with my work in Los Alamos. I worked mostly on the complexity aspect of Sequential Dynamical Systems (SDS). Briefly, SDSs are a formal model of computer simulation (somewhat like cellular automata) proposed by Los Alamos researchers. I won't tell you more about it (if you are curious as to what they are, read this survey). Anyway, in retrospect Los Alamos was a nice place to visit. The scenery was awesome, the people were friendly, and you can do some cool research there. [Fortunately, what Jon said didn't happen to me or any of my friends.] The down side, however, is that there is pretty much nothing else in Los Alamos. The town is practically dead after 6 --- there is virtually nobody walking on the street. And ... to my surprise, there was no shopping mall whatsoever in Los Alamos. One has to go to Santa Fe, which is the closest biggest city to Los Alamos, to find the nearest shopping mall. Anyway, I will put some pictures from my stay in Los Alamos when I finish developing the pictures.
It is a nice feeling to know that I will be doing logic on a regular basis from this time onwards. I arrived in Toronto last Saturday to start my graduate studies. I haven't completely settled yet, but I couldn't help myself blogging again after the internet connection was set up in my apartment here. Incidentally, this week is Toronto's Computer Science Department's orientation week. I am so happy to meet many logicians here, including some of the most well-known ones. For instance, Moshe Vardi (Rice University) came to visit this Tuesday and gave a talk outlining the development of logic and how computer science was born. I, and I believe most people in the audience (including the non-logicians), found the talk extremely entertaining and insightful. As my advisor, Leonid Libkin, put it this morning, Vardi has the rare gift to be both a top-notch researcher and an excellent speaker. [As you and I know, most researchers who do great research are poor at explaining their research to others.]
Anyhow, that is all I have for now. As a final remark, I haven't forgotten about my favourite logic of the month and will write on it some time next week after I have completely settled.
A little bit about my summer internship in Los Alamos ... I'll start with my work in Los Alamos. I worked mostly on the complexity aspect of Sequential Dynamical Systems (SDS). Briefly, SDSs are a formal model of computer simulation (somewhat like cellular automata) proposed by Los Alamos researchers. I won't tell you more about it (if you are curious as to what they are, read this survey). Anyway, in retrospect Los Alamos was a nice place to visit. The scenery was awesome, the people were friendly, and you can do some cool research there. [Fortunately, what Jon said didn't happen to me or any of my friends.] The down side, however, is that there is pretty much nothing else in Los Alamos. The town is practically dead after 6 --- there is virtually nobody walking on the street. And ... to my surprise, there was no shopping mall whatsoever in Los Alamos. One has to go to Santa Fe, which is the closest biggest city to Los Alamos, to find the nearest shopping mall. Anyway, I will put some pictures from my stay in Los Alamos when I finish developing the pictures.
It is a nice feeling to know that I will be doing logic on a regular basis from this time onwards. I arrived in Toronto last Saturday to start my graduate studies. I haven't completely settled yet, but I couldn't help myself blogging again after the internet connection was set up in my apartment here. Incidentally, this week is Toronto's Computer Science Department's orientation week. I am so happy to meet many logicians here, including some of the most well-known ones. For instance, Moshe Vardi (Rice University) came to visit this Tuesday and gave a talk outlining the development of logic and how computer science was born. I, and I believe most people in the audience (including the non-logicians), found the talk extremely entertaining and insightful. As my advisor, Leonid Libkin, put it this morning, Vardi has the rare gift to be both a top-notch researcher and an excellent speaker. [As you and I know, most researchers who do great research are poor at explaining their research to others.]
Anyhow, that is all I have for now. As a final remark, I haven't forgotten about my favourite logic of the month and will write on it some time next week after I have completely settled.
Tuesday, June 07, 2005
Interning in Los Alamos National Laboratory
Howdy! I have just recently started a summer research internship in Los Alamos National Laboratory. As my summer research topic is not directly related to logic, I will probably have to switch to a hibernation mode as far as blogging Logicomp is concerned. I will definitely resume with Logicomp when I start my graduate studies in Toronto (early September). One interesting thing that I plan to post on Logicomp in the future is the "Favorite Logic of the Month" in which I will mention my favorite logic of that month and a general method for proving (in)expressibility.
Anyway, until then I hope everyone have a great time!
Anyway, until then I hope everyone have a great time!
Subscribe to:
Posts (Atom)