.. 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
deduction_for_propositional_logic
propositional_logic_in_lean
first_order_logic
implementing_first_order_logic
decision_procedures_for_first_order_logic
using_smt_solvers
deduction_for_first_order_logic
using_first_order_theorem_provers
first_order_logic_in_lean
simple_type_theory
.. * :ref:`genindex`
* :ref:`modindex`
* :ref:`search`