Theorem proving calculi as decision procedures - The case of divisible torsion-free abelian groups

greatly enhanced by integrating specific algebraic routines,
such as, for instance, dedicated inference rules for abelian
groups or variable elimination algorithms. We present such
a calculus for divisible torsion-free abelian groups and
show that it is not only refutationally complete (even in
the presence of arbitrary free function symbols), but that
it is also a decision procedure for the theory of divisible
torsion-free abelian groups.

[Note: Talk moved from 16:15 to 17:15 to prevent a clash with
a PhD colloquy.]