# HG changeset patch
# User kono
# Date 979837407 -32400
# Node ID 029b5a5ac4943f8e0faf47a2515793454bbbc6aa
# Parent  1c57a78f1d9810fc9378f38a089642fbb34beb8a
*** empty log message ***

diff -r 1c57a78f1d98 -r 029b5a5ac494 problems
--- a/problems	Thu Jan 18 23:27:24 2001 +0900
+++ b/problems	Fri Jan 19 02:03:27 2001 +0900
@@ -1,3 +1,51 @@
+
+http://research.commpaq.com/SRC/esc/
+
+Fri Jan 19 01:20:54 JST 2001
+
+ω区間は、必ず、(s_n...s_m)* を含む。decidableならば、そうだ。
+が、それは、証明が必要がだけど。
+
+逆に、(s_n...s_m)* を含めば、そこをずーっと繰り返すことにより、
+ω区間を実装できる。だから、そういうループを見つければ、
+ω区間上で satisfiable だということができる。
+
+その区間上で、∨empty のようなexitが許されるのか? たぶん、
+許されない。ということは、やはり、false loop を見つければ
+良いと言うことか。
+
+そのアルゴリズムは?
+
+ω区間では、empty で抜け出ることができない。->
+   <>empty がfalse
+どうも正しそうだな。
+
+Fri Jan 19 00:33:43 JST 2001
+
+えーと、
+	[](false)
+がsatisfiableになることはない。
+	~(true & ~ false)
+	~(true & true)
+だから。
+	true & ~true
+は、許される。しかし、
+	~true & ~true
+は許されない。これ自体は、今のverifier でも、そうなる。
+
+tableau expansion 自体は同じだと考えて良いのか?
+特に異なる inference rule があるわけではないらしい。
+
+だとすれば、必要なコードは、false loop detector だけか?
+exe/diag の代りに、infinite_exe,infinite_diag を作るのだろうか。
+
+infinite_exe は、ループを表示しなければならない。必ず、
+そのようなループが存在するのだろうか? とすると、infinite
+interval は、prefix のようなものになる。実は、prefix
+がinfinite interval そのもの? prefix(finite,....)
+みたいなものだね。これは、どっかで見たことが...
+
+
 Thu Jan 18 22:42:24 JST 2001
 
 | ?- ex(((true&false)->(<>(empty)))).