3

現在、Java で自動化された定理証明に取り組んでいます。

これらのプルーフを PDF としてレンダリングできるようにしたいと考えています。できれば、これは、 proof.styまたはqtree.styを使用して、LaTeX のようなものを経由します。ただし、Java からの LaTeX コードのレンダリングには少し問題がある可能性があることを読みました。

Java では、証明は次のように、Haskell ツリーに着想を得た単純なツリーで表されます。

class Tree<A> {
  A       value;
  List<A> subForest;
}

これを最善の方法で実行する方法について誰かアイデアがありますか?

関連するメモ (つまり、すべて失敗するソリューション) でpdflatex、Java から実行可能ファイルを呼び出すためのベスト プラクティスは何ですか? （場所を特定する、存在するかどうかを調べるなど...）

4

1 に答える 1

4

jprocを使用して pdflatex を実行できます。タイムアウトを指定して、stdout と stderr の処理とリターン コードの解釈を処理できます。-interaction=batchmode パラメータを指定して pdflatex を起動して、エラーごとに停止しないようにしてください。さらに、速度や文字列テンプレートなどのテンプレート エンジンを使用してラテックスの入力を生成することをお勧めします。別の方法として、ラテックス式に Java API を提供することを目的とした jlatexmath を参照することもできます。

于 2011-01-26T10:32:11.433 に答える