Proofs and Explanations
=======================

This section focuses on higher-level reasoning outputs: abductive
explanations, Craig interpolants, and interactive proof construction. Core
reasoning infrastructure such as SRK and unification is documented in
:doc:`../logic-and-solving/index`.

.. toctree::
   :maxdepth: 2

   abduction
   interpolant
   itp