Overview
Atlassian Sourcetree is a free Git and Mercurial client for Windows.
Atlassian Sourcetree is a free Git and Mercurial client for Mac.
BEAGLE  a theorem prover for hierarchic superposition
Beagle is an automated theorem prover for firstorder logic with equality over linear integer/rational/real arithmetic. It accepts formulas in the FOF, TFF, and TFFINT formats of the TPTP syntax. It also accepts SMTLIB version 2 input files. See the SMTtoTPTP tool for more details on this.
A more experimental version of Beagle is maintained at https://bitbucket.org/joshbax189/beagle .
Warning
Beagle is currently not suitable for "big" input formulas. In particular the preprocessing algorithms are not optimized for that case. Beagle is intended as a testbed for theorem proving modulo arithmetic background theories. For problems without arithmetics there are better provers than Beagle.
Installation
Beagle is available at https://bitbucket.org/peba123/beagle . The distribution includes a precompiled jar archive and the Scala sources.
Running the precompiled Java archive
Run
java jar /PATH/TO/HERE/target/scala2.11/beagle.jar [OPTION...] FILE
where FILE is an SMTLIB version 2 or a TPTP TFF file.
See the examples
subdirectory for some test problems.
Run
java jar /PATH/TO/HERE/target/scala2.11/beagle.jar help
to obtain basic usage information.
Installation from sources
Beagle can be built with sbt, the Scala Build Tool. The sbt tool installs the scala compiler, if needed.
If Beagle is to be compiled onceandforall probably the easiest way is to create a Java jararchive and execute that. Steps:
(1) Install sbt.
(2) In the current directory invoke sbt assembly
.
If successful, this creates the file target/scala2.11/beagle.jar
Caveat: the file project/plugins.sbt
contains a line like
addSbtPlugin("com.eed3si9n" % "sbtassembly" % "0.9.2")
Please update the specified version string (here: "0.9.2") with a more recent one from https://github.com/sbt/sbtassembly should this version not be available.
(3) Run
java jar PATH/TO/HERE/target/scala2.11/beagle.jar [OPTION...] FILE
as described above.
Alternatively to (2) above, sbt compile
compiles the sources into Scala
class files. Assuming a Scala 2.11 runtime environment is installed, the
supplied shell script beagle
can then be used instead of (3). Run
/PATH/TO/HERE/beagle help
to get some basic usage information.
Background reasoning through SMT solvers
Beagle depends on an external SMT solver for the background theories of (linear) real arithmetics. For linear integer/rational arithmetic no external SMT solver is required, but one can be used instead of the builtin solvers. The SMT solver must be installed separately, it is not included in this distribution.
The SMT solver must comply with the SMTLIB
standard, version 2. Its invocation is specified by the Beagle flag
smtsolver
flag, e.g.,
beagle smtsolver /usr/local/bin/cvc4 FILE
Beagle calls the SMT solver via an SMTLIB file and receives its result from standard output. The SMT solver must accept its input file name as its last argument. Beagle tests if the SMT solver supports the computation of unsatisfiable cores and, if so, makes use of them.
Suitable SMT solvers are, e.g., CVC4 and Z3.
Notice that when specified, the SMT solver is also used for linear
integer/rational arithmetic. This behaviour can be overridden for linear
integer arithmetic by the liasolver
flag and specifying either iQE
or
cooper
(iQE
is highly experimental, not recommended).
Example:
beagle smtsolver /usr/local/bin/cvc4 liasolver iQE FILE
Running out of memory
Occasionally it is helpful to enable higher ressource limits. If you are encountering, e.g., heap problems, try adding the option
Xms512M Xmx4G Xss10M XX:MaxPermSize=384M
to the java call.
Documentation
Documentation beyond beagle help
is not yet available.
Precedences
Beagle, a superposition prover, works internally with term orderings (LPO if theories are present, KBO otherwise). The precedences among operators for LPO can be specified in the input TPTP file as follows:
%$ :prec f > g > h %$ :prec f > k > l
Beagle will linearize the stated precedences into a total ordering on operator symbols.
The corresponding syntax in SMTLIB input files is as follows:
(setoption :prec ("f > g > h" "f > k > l"))
Refutations
Beagle is capable of generating refutations from successful proof attempts.
There are currently three ways to display refutations:
beagle proof
print a plain text refutation to stdout
beagle proof print tff
print a TFF formatted refutation to stdout
* beagle prooffile [file_name]
write both a type signature and refutation in TFF format to the specified file
In addition Beagle will produce a TFF formatted description of a saturated set if found when the print tff
flag is set.
Note that these refutations do not typically include detailed descriptions of CNF translations or detailed theory reasoning.
Publications

Peter Baumgartner, Joshua Bax, Uwe Waldmann. Beagle  A Hierarchic Superposition Theorem Prover. This is the main paper on Beagle. Please use the following Bibtex entry for citations:
@inproceedings{Baumgartner:Bax:Waldmann:Beagle:CADE:2015, author = {Peter Baumgartner and Joshua Bax and Uwe Waldmann}, title = {{Beagle}  {A} {H}ierarchic {S}uperposition {T}heorem {P}rover}, booktitle = {CADE25  25th International Conference on Automated Deduction}, editor = {Amy P. Felty and Aart Middeldorp}, year = {2015}, series = {LNAI}, volume = {9195}, pages = {367377} }

Peter Baumgartner, Uwe Waldmann. Hierarchic superposition with weak abstraction

Peter Baumgartner, Joshua Bax, Uwe Waldmann. Finite Quantification in Hierarchic Theorem Proving

Peter Baumgartner, Joshua Bax. Proving Infinite Satisfiability
Contact
Email: Peter.Baumgartner@nicta.com.au
Usage reports, comments and suggestions are gratefully received.