問題タブ [horn]

最近、HORN について少し耳にするようになりましたが、HORN がどのような問題を解決できるのか、実際の状況で HORN を使用するとどのように役立つのか知りたいと思っています。

http://code.google.com/p/hornget/

NHibernate 2.1 の最近のアップグレードにより、大きな頭痛の種が表面化しました。

ほとんどのプロジェクトは、署名済みアセンブリとしてデフォルトでビルドされているようです。たとえば、fluentnhibernate はキーファイル fluent.snk を参照します。

Nhibernate.search は、収集できるものから署名なしでビルドされ、署名付きでビルドされません。つまり、生成されたキーファイルを参照すると、次のエラーが発生します。

参照されたアセンブリ 'Lucene.Net' には厳密な名前がありません

これは、依存関係として nhibernate.search を持つ Castle.activerecord のようなプロジェクトは、アセンブリ nhibernate.search に厳密な名前がありません: という恐ろしいエラーが発生するため、ビルドされないことを意味します。

かなりの数のプロジェクトが caslte.activerecord を使用しているため、これをビルドすることが非常に重要です。

私は完全にアイデアがないので、ここで何をすべきか誰か考えていますか?

これは完全な狂気です。

ホーン式が充足可能かどうかを証明する方が簡単であることはわかっています。私の質問は: 通常の CNF よりもホーン式の方が簡単なのはなぜですか?

この codepen に見られるような効果を作成することを目指しています。背景ビデオの上に透明な SVG があります。これまでのところ、Photoshop からエクスポートしたパス形状が選択された AI ドキュメントがあります。理想的には、パスの内側を透明にしたいのですが、残りは例のように白くします。どうすればこのような効果を達成できますか?

このコード行と関係があるように見えますが、私は間違いなく何かを誤解しています。

SVG はパスだけでは準備ができていないと思います。エクスポートした場合は空白として表示され、パスにストロークを配置すると、ストローク以外のすべてが透明であるか、透明度が表示されないためです。まったく。

通常、Web 開発者としての私のワークフローでは、SVG でこれを詳細に作業することは決してないため、これには少し行き詰まっています。

Z3 と拡張 SMT-LIB2 構文を使用してホーン句を解決しています。角節の先頭は解釈されない述語であるべきだということはわかっています。しかし、次の節をどのようにホーン節の集合に書き直せばよいのだろうか。

Z3(> a 0)は、ホーン節の先頭になれないと不平を言っています。最後の節を次のように書き直すことができます。

しかし、その後、句が非常に弱くなり、 invariant の意図したモデルが得られなくなりますinv。これを行うためのより良い方法があるかどうか疑問に思います。