tag:blogger.com,1999:blog-12932458.post112898056113603657..comments2023-09-29T09:03:36.236-05:00Comments on Logicomp: Favorite Logic of September 2005: First-order Logic (2)anthonywlinhttp://www.blogger.com/profile/07618509800342861247noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-12932458.post-1129040152600960472005-10-11T09:15:00.000-05:002005-10-11T09:15:00.000-05:00Jon: thanks! Yes, you are right! It's all fixed no...Jon: thanks! Yes, you are right! It's all fixed now. I guess I was really careless on my second attempt to post about model-checking (the first one got erased abruptly because of a bug in my firefox).<BR/><BR/>On a related note, if M is infinite and we can represent it finitely, checking M |= f might still be decidable. This issue is studied in "Embedded Finite Model Theory", see Libkin's book.anthonywlinhttps://www.blogger.com/profile/07618509800342861247noreply@blogger.comtag:blogger.com,1999:blog-12932458.post-1128993973022416082005-10-10T20:26:00.000-05:002005-10-10T20:26:00.000-05:00Nice post Anthony! Some pedantism from me...we wan...Nice post Anthony! Some pedantism from me...<BR/><BR/><I>we want to test whether `M |= f`, i.e., `M` is true in `f`</I><BR/><BR/>Perhaps that f is true in M rather?<BR/><BR/><I>Immeadiately, I hear you say that this problem is trivially decidable...</I><BR/><BR/>Well, so long as you take M to be finite :-)Anonymousnoreply@blogger.com