方針2021 03

今後どうしていきたいか(2021/3/06)

そこでできていることは次のとおり。

やってみたいことをひととおりやる。(下記)
package化。最小機能のexport。
system化。
主要機能のテスト(itoによる定義) 外部に依存せずにどうやって動作確認ができるのかにちゃんと取り組む気持ちになったらする。機能が増えてきたのでなかなかできていない。
ドキュメント(最低限)

やってみたいことは、永遠になくならないかもしれないが、いずれ自分でもわからなくなるはずなので、これは2021/12/31を期限とする。
package化は、自分にメリットがあるかどうかわからないが、3/14までにしよう。自分にメリットがあるかどうかというのは、exportしていないsymbolのテストが動かなくなったりすると面倒ということ。
system化はファイル構成が存在すればできるので3/7 明日までにしよう。asdfは使える。
難問・・・今日は結論だせない。
ドキュメントはときどき書いているから、それでいいかも。

DLとProverの結合。DLは、世界の情報を取り出すセンサーであり、世界から命題を作り出す装置と考える。Proverはそこから既存の知識で推論する。何が生まれるのか?
動的Axiom系。新しい命題が追加されていくProver/Axiomシステム。矛盾したり、拡張したり。
有限ドメインのいろいろな複雑さ(有限群をドメインとすれば単純な表現になるということか?)
WebUI(JuliaでやったView)

FOLは演繹システムなので新しい情報を生み出さない。世界の生み出す新しい変化をDLが新しい情報として取り出し、FOLに渡す。という枠組み。 FOLはそこでどういう役に立つのか?

公理系Aに新たに命題bを追加したとき、どうするか。

有限ドメイン固有の性質をどうするか。

例えば、もしxのドメインDが{a,b}の場合、aとbが排他的であるつまり、+P(a)≡-P(b)がなりたつのであれば

<+P(a):-P(b)>はsemanticalには[]になる。

というようなこと。

でもこれははかない。{a,b,c}になったとたん世界がかわってしまう。

そのはかなさをどうするのか。

JuliaではGenieをもとにviewlogicが作れた。

同じように、commonlispではcaveman2が使えるらしい。これでviewlogic相当のものを作りたい(cheapview?)