aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proofs/automatic-tactics/index.rst
blob: e458c3a9f509b2619a9cf19d36105a6846742f57 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
.. _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