Merge pull request #149 from daviddoret/dev

merge dev in qa

docs/build/.buildinfo

@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 7f2341602339f5787e05519e6e1924b2
+config: 32dd555d207fe9d43466c601a4446270
 tags: 645f666f9bcd5a90fca523b33c5a78b7

docs/build/_sources/bibliography.rst.txt

@@ -5,4 +5,4 @@
     ************
 
 .. bibliography:: bibliography_bibtex.bib
-   :style: plain
+   :cited:

docs/build/_sources/disjunction_elimination.rst.txt

@@ -0,0 +1,2 @@
+disjunction-elimination
+=========================

docs/build/_sources/elimination_rule.rst.txt

@@ -7,7 +7,7 @@ Definition
 An *introduction-rule* is an :doc:`inference_rule` that allows to derive a formula-statement of some syntactic form from some define premises.
 
 List of well-known *introduction-rules*
---------------------------------------
+------------------------------------------
 
 * :doc:`biconditional_elimination_left`
 * :doc:`biconditional_elimination_right`

docs/build/_sources/formula_statement.rst.txt

@@ -0,0 +1,3 @@
+formula-statement
+===================
+

docs/build/_sources/hypothesis.rst.txt

@@ -0,0 +1,3 @@
+hypothesis
+============
+

docs/build/_sources/inconsistency_introduction_1.rst.txt

@@ -0,0 +1,38 @@
+inconsistency-introduction-1
+========================================
+
+Definition
+----------
+
+*inconsistency-introduction-1* is the :doc:`inference_rule`:
+
+.. math::
+
+   \left( P, \neg \left(P\right) \right) \vdash Inc\left(\mathcal{T}\right)
+
+In straightforward language, if we prove a proposition and its negation, it follows that the theory is inconsistent.
+
+Quotes
+------
+
+Python sample usage
+----------------------
+
+.. admonition:: Source code
+  :class: tip, dropdown
+
+   .. literalinclude :: ../../sample/code/inconsistency_introduction_1.py
+      :language: python
+      :linenos:
+
+.. admonition:: Unicode output
+   :class: note, dropdown
+
+   .. literalinclude :: ../../sample/output/inconsistency_introduction_1_unicode.txt
+      :language: text
+
+.. admonition:: Plaintext output
+   :class: note, dropdown
+
+   .. literalinclude :: ../../sample/output/inconsistency_introduction_1_plaintext.txt
+      :language: text

docs/build/_sources/inconsistency_introduction_2.rst.txt

@@ -0,0 +1,41 @@
+inconsistency-introduction-2
+========================================
+
+Definition
+----------
+
+*inconsistency-introduction-2* is the :doc:`inference_rule`:
+
+.. math::
+
+   \left(\left(x = y\right), \left(x \neq y\right)\right) \vdash Inc\left(\mathcal{T}\right)
+
+In straightforward language, if we prove both the equality and inequality of two terms, it follows that the theory is inconsistent.
+
+Quotes
+----------
+
+   A proof of consistency will have to show, by appealing to contentual considerations which are completely unproblematic, that in the formalism in question it is never possible to derive the formula 𝑎 ≠ 𝑎, or alternatively it is not possible to prove both 𝑎 = 𝑏 and 𝑎 ≠ 𝑏. :cite:p:`mancosu_2021_introductionprooftheorynormalization{p. 5}`
+
+
+Python sample usage
+----------------------
+
+.. admonition:: Source code
+  :class: tip, dropdown
+
+   .. literalinclude :: ../../sample/code/inconsistency_introduction_2.py
+      :language: python
+      :linenos:
+
+.. admonition:: Unicode output
+   :class: note, dropdown
+
+   .. literalinclude :: ../../sample/output/inconsistency_introduction_2_unicode.txt
+      :language: text
+
+.. admonition:: Plaintext output
+   :class: note, dropdown
+
+   .. literalinclude :: ../../sample/output/inconsistency_introduction_2_plaintext.txt
+      :language: text

docs/build/_sources/inconsistency_introduction_3.rst.txt

@@ -0,0 +1,41 @@
+inconsistency-introduction-3
+========================================
+
+Definition
+----------
+
+*inconsistency-introduction-3* is the :doc:`inference_rule`:
+
+.. math::
+
+   \left( P \neq P \right) \vdash Inc\left(\mathcal{T}\right)
+
+In straightforward language, if we prove that an object is not equal to itself, it follows that the theory is inconsistent.
+
+Quotes
+----------
+
+   A proof of consistency will have to show, by appealing to contentual considerations which are completely unproblematic, that in the formalism in question it is never possible to derive the formula 𝑎 ≠ 𝑎, or alternatively it is not possible to prove both 𝑎 = 𝑏 and 𝑎 ≠ 𝑏. :cite:p:`mancosu_2021_introductionprooftheorynormalization{p. 5}`
+
+
+Python sample usage
+----------------------
+
+.. admonition:: Source code
+  :class: tip, dropdown
+
+   .. literalinclude :: ../../sample/code/inconsistency_introduction_3.py
+      :language: python
+      :linenos:
+
+.. admonition:: Unicode output
+   :class: note, dropdown
+
+   .. literalinclude :: ../../sample/output/inconsistency_introduction_3_unicode.txt
+      :language: text
+
+.. admonition:: Plaintext output
+   :class: note, dropdown
+
+   .. literalinclude :: ../../sample/output/inconsistency_introduction_3_plaintext.txt
+      :language: text

docs/build/_sources/index.rst.txt

@@ -13,24 +13,38 @@ Welcome to punctilious's documentation!
    :maxdepth: 1
    :caption: Contents:
 
+   test
+
    absorption
    bibliography
+   biconditional_elimination_left
+   biconditional_elimination_right
+   biconditional_introduction
    conjunction_elimination_left
    conjunction_elimination_right
    conjunction_introduction
+   disjunction_elimination
    disjunction_introduction_left
    disjunction_introduction_right
    double_negation_elimination
    double_negation_introduction
    elimination_rule
-   inconsistency_by_inequality_introduction
+   formula_statement
+   hypothesis
+   inconsistency_introduction_1
+   inconsistency_introduction_2
+   inconsistency_introduction_3
    inference_rule
    introduction_rule
    is_a
    meta_object
    modus_ponens
    notation_form
    paragraph_proof
+   proof_by_contradiction_1
+   proof_by_contradiction_2
+   proof_by_refutation_1
+   proof_by_refutation_2
    relation
    theory_elaboration_sequence
    universe_of_discourse

docs/build/_sources/introduction_rule.rst.txt

@@ -7,7 +7,7 @@ Definition
 An *introduction-rule* is an :doc:`inference_rule` that allows to derive a formula-statement of some syntactic form from some define premises.
 
 List of well-known *introduction-rules*
---------------------------------------
+-----------------------------------------
 
 * :doc:`biconditional_introduction`
 * :doc:`conjunction_introduction`

docs/build/_sources/proof_by_contradiction_1.rst.txt

@@ -0,0 +1,35 @@
+proof-by-contradiction-1
+=========================
+
+Definition
+-----------
+
+*proof-by-contradiction-1* is the :doc:`inference_rule`:
+
+.. math::
+
+    \left( \mathcal{H} assume \not \mathbf{P}, Inc\left(\mathcal{H}\right)  \right) \vdash \mathbf{P}
+
+Python implementation
+----------------------
+
+Sample usage
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. literalinclude :: ../../sample/code/proof_by_contradiction_1.py
+   :language: python
+
+.. literalinclude :: ../../sample/output/proof_by_contradiction_1_unicode.txt
+   :language: text
+
+Documentation
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+.. module:: core
+    :noindex:
+.. autoclass:: InferenceRuleInclusionDict
+    :members: proof_by_contradiction_1
+
+Bibliography
+------------
+
+.. footbibliography::

docs/build/_sources/proof_by_contradiction_2.rst.txt

@@ -0,0 +1,35 @@
+proof-by-contradiction-2
+=========================
+
+Definition
+----------
+
+*proof-by-contradiction-2* is the :doc:`inference_rule`:
+
+.. math::
+
+    \left( \mathcal{H} assume \not \mathbf{P}, Inc\left(\mathcal{H}\right)  \right) \vdash \mathbf{P}
+
+Python implementation
+---------------------
+
+ProofByContradiction2Declaration
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. module:: core
+    :noindex:
+.. autoclass:: ProofByContradiction2Declaration
+    :members:
+    :special-members: __init__
+
+ProofByContradiction2Inclusion
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. autoclass:: ProofByContradiction2Inclusion
+    :members:
+    :special-members: __init__
+
+Bibliography
+------------
+
+.. footbibliography::

docs/build/_sources/proof_by_refutation_1.rst.txt

@@ -0,0 +1,41 @@
+proof-by-refutation-1
+=========================
+
+Definition
+----------
+
+*proof-by-refutation-1* is the :doc:`inference_rule`:
+
+.. math::
+
+    \left( \boldsymbol{\mathcal{H}} \: \textit{assume} \: \neg \boldsymbol{P}, \boldsymbol{P}, Inc\left( \boldsymbol{\mathcal{H}} \right)  \right) \vdash \boldsymbol{P}
+
+Where:
+ * :math:`\boldsymbol{\mathcal{H}}` is an :doc:`hypothesis`
+ * :math:`\boldsymbol{P}` is a :doc:`formula_statement`
+
+In plain language, it consists in posing the hypothesis that a proposition :math:`\boldsymbol{P}` is not true, refuting that hypothesis by proving :math:`\boldsymbol{P}`, inferring the inconsistency of that hypothesis from this contradiction, and finally inferring :math:`\boldsymbol{P}`.
+
+Python implementation
+---------------------
+
+ProofByRefutation1Declaration
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. module:: core
+    :noindex:
+.. autoclass:: ProofByRefutation1Declaration
+    :members:
+    :special-members: __init__
+
+ProofByRefutation1Inclusion
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. autoclass:: ProofByRefutation1Inclusion
+    :members:
+    :special-members: __init__
+
+Bibliography
+------------
+
+.. footbibliography::

docs/build/_sources/proof_by_refutation_2.rst.txt

@@ -0,0 +1,35 @@
+proof-by-refutation-2
+=========================
+
+Definition
+----------
+
+*proof-by-refutation-2* is the :doc:`inference_rule`:
+
+.. math::
+
+    \left( \mathcal{H} assume \not \mathbf{P}, Inc\left(\mathcal{H}\right)  \right) \vdash \mathbf{P}
+
+Python implementation
+---------------------
+
+ProofByRefutation2Declaration
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. module:: core
+    :noindex:
+.. autoclass:: ProofByRefutation2Declaration
+    :members:
+    :special-members: __init__
+
+ProofByRefutation2Inclusion
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. autoclass:: ProofByRefutation2Inclusion
+    :members:
+    :special-members: __init__
+
+Bibliography
+------------
+
+.. footbibliography::

docs/build/_sources/test.rst.txt

@@ -0,0 +1,5 @@
+minimalist example
+=====================
+
+.. literalinclude :: ../../sample/output/proof_by_contradiction_1_unicode.txt
+   :language: text

docs/build/_static/css/custom.css

@@ -0,0 +1,11 @@
+/*
+Fix to assure text wrapping in code and code output inclusions implemented with the literalinclude sphinx directive.
+References:
+ - https://docs.readthedocs.io/en/stable/guides/adding-custom-css.html
+ - https://stackoverflow.com/questions/66971299/sphinx-documentation-with-readthedocs-theme-text-block-wrapping
+ - https://stackoverflow.com/questions/46800045/how-to-wrap-a-long-literal-block-in-restructuredtext
+*/
+pre {
+    white-space: pre-wrap !important;
+    word-break: break-all;
+}