1. Peter Baumgartner
  2. Beagle

Overview

HTTPS SSH

BEAGLE - a theorem prover for hierarchic superposition

Beagle is an automated theorem prover for first-order logic with equality over linear integer/rational/real arithmetic. It accepts formulas in the FOF, TFF, and TFF-INT formats of the TPTP syntax. It also accepts SMT-LIB 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 pre-compiled jar archive and the Scala sources.

Running the pre-compiled Java archive

Run

java -jar /PATH/TO/HERE/target/scala-2.11/beagle.jar [OPTION...] FILE

where FILE is an SMT-LIB version 2 or a TPTP TFF file. See the examples subdirectory for some test problems.

Run

java -jar /PATH/TO/HERE/target/scala-2.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 once-and-forall probably the easiest way is to create a Java jar-archive and execute that. Steps:

(1) Install sbt.

(2) In the current directory invoke sbt assembly.

If successful, this creates the file target/scala-2.11/beagle.jar

Caveat: the file project/plugins.sbt contains a line like

addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.9.2")

Please update the specified version string (here: "0.9.2") with a more recent one from https://github.com/sbt/sbt-assembly should this version not be available.

(3) Run

java -jar PATH/TO/HERE/target/scala-2.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 built-in solvers. The SMT solver must be installed separately, it is not included in this distribution.

The SMT solver must comply with the SMT-LIB 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 SMT-LIB 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 SMT-LIB input files is as follows:

(set-option :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 -proof-file [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

Contact

Peter Baumgartner

Email: Peter.Baumgartner@nicta.com.au

Usage reports, comments and suggestions are gratefully received.