7 Availability
Beagle is available at https://bitbucket.org/peba123/beagle under a GNU Gen-
eral Public license. The distribution includes the Scala source code and a ready-to-
run Java jar-file. A more experimental version of Beagle is maintained at https:
//bitbucket.org/joshbax189/beagle.
References
1. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection
and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.
2. L. Bachmair, H. Ganzinger, and U. Waldmann. Refutational theorem proving for hierarchic
first-order theories. Appl. Algebra Eng. Commun. Comput, 5:193–212, 1994.
3. C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi
´
c, T. King, A. Reynolds, and
C. Tinelli. CVC4. In CAV, volume 6806 of LNCS 6806, pp. 171–177. Springer, 2011.
4. C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0. In A. Gupta and
D. Kroening, eds., SMT Workshop, 2010.
5. P. Baumgartner. SMTtoTPTP – A Converter for Theorem Proving Formats. In A. Felty and
A. Middeldorp, eds., CADE-25, LNAI. Springer, 2015.
6. P. Baumgartner, J. Bax, and U. Waldmann. Finite Quantification in Hierarchic Theorem
Proving. In S. Demri, D. Kapur, and C. Weidenbach, eds., IJCAR 2014, LNAI 8562, pp.
152–167. Springer, 2014.
7. P. Baumgartner and U. Waldmann. Hierarchic Superposition With Weak Abstraction. In
M. P. Bonacina, editor, CADE-24, LNCS 7898, pp. 39–57. Springer, 2013.
8. D. C. Cooper. Theorem Proving in Arithmetic Without Multiplication. In Machine Intelli-
gence, volume 7, pages 91–99, New York, 1972. American Elsevier.
9. B. Dutertre and L. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In CAV, LNCS
4144, pp. 81–94, Springer, 2006.
10. J. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University
Press, 2009.
11. E. Kruglov and C. Weidenbach. Superposition Decides the First-Order Logic Fragment Over
Ground Theories. Mathematics in Computer Science, pp. 1–30, 2012.
12. L. M. de Moura and N. Bjørner. Z3: An efficient smt solver. In C. R. Ramakrishnan and
J. Rehof, eds., TACAS, LNCS 4963, pp 337–340. Springer, 2008.
13. V. Prevosto and U. Waldmann. SPASS+T. In G. Sutcliffe, R. Schmidt, and S. Schulz, eds.,
ESCoR: Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings,
pp. 18–33, Seattle, WA, USA, 2006.
14. W. Pugh. The Omega Test: A Fast and Practical Integer Programming Algorithm for Depen-
dence Analysis. In ACM/IEEE conference on Supercomputing, pp. 4–13. ACM, 1991.
15. P. R
¨
ummer. A Constraint Sequent Calculus for First-Order Logic With Linear Integer Arith-
metic. In I. Cervesato, H. Veith, and A. Voronkov, eds., LPAR, LNCS 5330, pp. 274–289.
Springer, 2008.
16. SMT-LIB, The Satisfiability Modulo Theories Library. http://smt-lib.org/.
17. G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: The FOF and CNF
Parts, v3.5.0. Journal of Automated Reasoning, 43(4):337–362, 2009.
18. G. Sutcliffe. The 7th IJCAR Automated Theorem Proving System Competition - CASC-J7.
AI Communications, 28:To appear, 2015.
19. G. Sutcliffe, S. Schulz, K. Claessen, and P. Baumgartner. The TPTP Typed First-order Form
with Arithmetic. In N. Bjørner and A. Voronkov, eds., LPAR-18, LNCS 7180. Springer, 2012.
10