.. Logic and Mechanized Reasoning documentation master file, created by
   sphinx-quickstart on Wed Jun  9 15:14:10 2021.
   You can adapt this file completely to your liking, but it should at least
   contain the root `toctree` directive.

Logic and Mechanized Reasoning
==============================

.. toctree::
   :maxdepth: 2
   :numbered:
   :caption: Contents:

   introduction
   mathematical_background
   using_lean_as_a_programming_language
   propositional_logic
   implementing_propositional_logic
   decision_procedures_for_propositional_logic
   using_sat_solvers
   proof_systems_for_propositional_logic
   using_lean_as_a_proof_assistant
   first_order_logic
   implementing_first_order_logic
   decision_procedures_for_first_order_logic
   using_smt_solvers
   proof_systems_for_first_order_logic
   using_first_order_theorem_provers
   beyond_first_order_logic

.. * :ref:`genindex`
   * :ref:`modindex`
   * :ref:`search`