Rendering PDF proofs with Java (via LaTex?)

Question

Currently I am working on a automated theorem prover in Java.

I would like to be able to render these proofs, as PDF. Preferrably, this will go though something like LaTeX, using proof.sty or qtree.sty. However, I've read that rendering LaTeX code from Java can be a bit problematic.

In Java, the proofs are represented by simple trees, inspired on the Haskell trees, as:

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

Has anybody got any ideas on how to best do this?

On a related note (i.e. the all-else-fails solution) what are the best practices for calling a pdflatex executable from Java? (As for locating it, figuring out whether or not it exists, etc...)

Answer 1

You could use jproc to run pdflatex. It let's you specify a timeout and takes care of processing stdout and stderr as well as interpreting the return code. Make sure that you launch pdflatex with -interaction=batchmode parameter, so it doesn't stop at every error. Furthermore I would recommend to use a templating engine like velocity or stringtemplate to produce the input for latex. Alternatively you might want to look at jlatexmath which aims at offering a java api to latex formulas.