coq is a formal proof management system. It provides a formal language
to write mathematical definitions, executable algorithms and theorems
together with an environment for semi-interactive development of
machine-checked proofs.

Unfortunately CoqIDE can no longer be built as it requires lablgtk3,
while only lablgtk2 is packaged in Slackware. You can however get
Coq 8.9 with CoqIDE. To do so, run this Slackbuild with VERSION=8.9
and COQIDE=yes (after getting the Coq 8.9 tarball). You will need to
install the gtksourceview package before building lablgtk.