diff options
Diffstat (limited to 'doc/sphinx/proofs/automatic-tactics/index.rst')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/index.rst | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst index a219770c69..c3712b109d 100644 --- a/doc/sphinx/proofs/automatic-tactics/index.rst +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -1,20 +1,22 @@ .. _automatic-tactics: ===================================================== -Built-in decision procedures and programmable tactics +Automatic solvers and programmable tactics ===================================================== Some tactics are largely automated and are able to solve complex -goals. This chapter presents both some decision procedures that can -be used to solve some specific categories of goals, and some -programmable tactics, that the user can instrument to handle some +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/omega ../../addendum/micromega ../../addendum/ring ../../addendum/nsatz + auto ../../addendum/generalized-rewriting |