<p>Similar questions come up every now and then, e.g. <a href="https://stackoverflow.com/q/40848265/4776939">here</a> and <a href="https://stackoverflow.com/q/30905122/4776939">there</a>. None of them talks about Java or Scheme though, so here's a slightly adapted answer for the "Java" part.</p>

<h2>Calling Isabelle from Java</h2>

<p>Isabelle itself has no "API" that can be called from external tools. The general philosophy is that applications should live inside Isabelle or the <a href="https://www.isa-afp.org/" rel="nofollow noreferrer">Archive of Formal Proofs</a>. Most of the time, this means your applications needs to be implemented in Isabelle/ML.</p>

<p>However, if you want to use Isabelle <em>as an external tool</em>, you have to play some tricks. I have bundled up these tricks as a Scala library (<a href="https://github.com/larsrh/libisabelle" rel="nofollow noreferrer">libisabelle</a>). An overview of how this works is given in <a href="https://arxiv.org/abs/1607.01539" rel="nofollow noreferrer">a paper</a>.</p>

<p>libisabelle itself is available as a stand-alone library including some basic documentation that should allow you to get started. See <a href="https://github.com/larsrh/libisabelle" rel="nofollow noreferrer">the repository</a> for more details. In essence, it allows you to</p>

<ul>
<li>manage Isabelle installations from within Scala (download, unpacking)</li>
<li>abstract over different Isabelle versions (currently supported: 2016 and 2016-1)</li>
<li>lifecycle management of an Isabelle session (building, starting, stopping)</li>
<li>treat Isabelle/ML functions as Scala functions</li>
<li>goodies like Isabelle term syntax in Scala (<code>term"$n &gt; 0 --&gt; ($b &amp; ${HOLogic.True})"</code>)</li>
</ul>

<p>There is no built-in routine to set up a goal state and apply some proof steps, but the necessary infrastructure is all there.</p>

<p>libisabelle is implemented in Scala, but there is a Java API that you can use, too. I know of one user who successfully uses that one. You can have a look at <a href="https://github.com/larsrh/libisabelle/blob/v0.8.0/modules/examples/src/main/java/edu/tum/cs/isabelle/examples/Hello_PIDE.java" rel="nofollow noreferrer">an example</a> in the repository.</p>
Calling Isabelle from external software (Java, Scheme)
<p>Is it possible to call Isabelle from external programms (Java, Scheme/Guile)? I have not managed to find documentation about API</p>