.. _automatic-tactics:

=====================================================
Automatic solvers and programmable tactics
=====================================================

Some tactics are largely automated and are able to solve complex
goals.  This chapter presents both built-in solvers that can
be used on specific categories of goals and
programmable tactics that the user can instrument to handle
complex goals in new domains.

.. toctree::
   :maxdepth: 1

   logic
   ../../addendum/micromega
   ../../addendum/ring
   ../../addendum/nsatz
   auto
   ../../addendum/generalized-rewriting