--- a/problems	Fri Jan 19 20:37:32 2001 +0900
+++ b/problems	Fri Jan 19 23:14:00 2001 +0900
@@ -1,3 +1,44 @@
+Fri Jan 19 20:59:46 JST 2001
+
+    | ?- ex((infinite -> @infinite)).
+
+    state(1 , not(true&false),@ (true&false))
+    [][empty]->empty
+    [][more]->true
+
+    0.021000000000000796 sec.
+    1 states
+    2 subterms
+    2 state transions
+    verbose,renaming,singleton,length limit 5
+    valid
+
+    yes
+    | ?- infinite.
+    unsatisfiable in infinite interval.
+
+これは... どういうことなんでしょうね? inifite は基本的に
+false だから、inifite-> タイプのものは、すべて、infinite unsatisfiable
+だね。
+
+Fri Jan 19 20:40:37 JST 2001
+
+割りと簡単なアルゴリズムで、satisfiabilityは、チェック
+できました。これが、正しいかどうかは Moszkowski によるけど...
+   inifnite
+   *skip
+   *((skip&skip))
+などに関しては、うまく動くようですね。
+
+vailidity checker が欲しい所だけど... どういうものがvalidなのかは、
+良くわからない。もちろん、否定が unsatisfiable ならば、valid なの
+だが。
+
+でも、この方法だと、
+    satisfiable in ω-interval implies
+      falsifiable in finite interval
+ってことになるらしい。
+
 Fri Jan 19 07:48:59 JST 2001
 
 Streett     ∩_i []<>L_i ⊃ <>[]U _i