issue #143: enhance disjunction-introduction (left and right) inferen…

…ce-rules + empty restructured pages to prepare the documentation of interence-rules
daviddoret · Aug 22, 2023 · 337d6fc · 337d6fc
1 parent cd0d2d4
commit 337d6fc
Show file tree

Hide file tree

Showing 24 changed files with 2,003 additions and 0 deletions.
diff --git a/docs/build/.doctrees/biconditional_elimination_left.doctree b/docs/build/.doctrees/biconditional_elimination_left.doctree
diff --git a/docs/build/.doctrees/biconditional_elimination_right.doctree b/docs/build/.doctrees/biconditional_elimination_right.doctree
diff --git a/docs/build/.doctrees/biconditional_introduction.doctree b/docs/build/.doctrees/biconditional_introduction.doctree
diff --git a/docs/build/.doctrees/conjunction_elimination_left.doctree b/docs/build/.doctrees/conjunction_elimination_left.doctree
diff --git a/docs/build/.doctrees/conjunction_elimination_right.doctree b/docs/build/.doctrees/conjunction_elimination_right.doctree
diff --git a/docs/build/.doctrees/double_negation_elimination.doctree b/docs/build/.doctrees/double_negation_elimination.doctree
diff --git a/docs/build/.doctrees/elimination_rule.doctree b/docs/build/.doctrees/elimination_rule.doctree
diff --git a/docs/build/.doctrees/introduction_rule.doctree b/docs/build/.doctrees/introduction_rule.doctree
diff --git a/docs/build/_sources/biconditional_elimination_left.rst.txt b/docs/build/_sources/biconditional_elimination_left.rst.txt
@@ -0,0 +1,2 @@
+biconditional-elimination-left
+===============================
diff --git a/docs/build/_sources/biconditional_elimination_right.rst.txt b/docs/build/_sources/biconditional_elimination_right.rst.txt
@@ -0,0 +1,2 @@
+biconditional-elimination-right
+===============================
diff --git a/docs/build/_sources/biconditional_introduction.rst.txt b/docs/build/_sources/biconditional_introduction.rst.txt
@@ -0,0 +1,2 @@
+biconditional-introduction
+===============================
diff --git a/docs/build/_sources/conjunction_elimination_left.rst.txt b/docs/build/_sources/conjunction_elimination_left.rst.txt
@@ -0,0 +1,2 @@
+conjunction-elimination-left
+===============================
diff --git a/docs/build/_sources/conjunction_elimination_right.rst.txt b/docs/build/_sources/conjunction_elimination_right.rst.txt
@@ -0,0 +1,2 @@
+conjunction-elimination-right
+===============================
diff --git a/docs/build/_sources/double_negation_elimination.rst.txt b/docs/build/_sources/double_negation_elimination.rst.txt
@@ -0,0 +1,2 @@
+double-negation-elimination
+===============================
diff --git a/docs/build/_sources/elimination_rule.rst.txt b/docs/build/_sources/elimination_rule.rst.txt
@@ -0,0 +1,28 @@
+elimination-rule
+==================
+
+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`
+* :doc:`conjunction_elimination_left`
+* :doc:`conjunction_elimination_right`
+* :doc:`disjunction_elimination`
+* :doc:`double_negation_elimination`
+
+Quotes
+-------
+
+    "Each of the introduction rules tells us how to derive a formula of some syntactic form. For instance, the conjunction introduction rule (∧I) shows that we can derive a conjunction if we derive both conjunctive terms; the disjunction introduction rules (∨I) show that we can derive a disjunction if we derive one of the disjunctive terms."
+    - :footcite:p:`porter_2008_handbookknowledgerepresentation`, p. 6-7
+
+Bibliography
+------------
+
+.. footbibliography::
diff --git a/docs/build/_sources/introduction_rule.rst.txt b/docs/build/_sources/introduction_rule.rst.txt
@@ -0,0 +1,33 @@
+introduction-rule
+==================
+
+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`
+* :doc:`disjunction_introduction_left`
+* :doc:`disjunction_introduction_right`
+* :doc:`double_negation_introduction`
+
+Quotes
+-------
+
+    "Each of the introduction rules tells us how to derive a formula of some syntactic form. For instance, the conjunction introduction rule (∧I) shows that we can derive a conjunction if we derive both conjunctive terms; the disjunction introduction rules (∨I) show that we can derive a disjunction if we derive one of the disjunctive terms."
+    - :footcite:p:`porter_2008_handbookknowledgerepresentation`, p. 6-7
+
+See also
+---------
+
+* :doc:`elimination_rule`
+* :doc:`inference_rule`
+
+Bibliography
+------------
+
+.. footbibliography::
diff --git a/docs/build/biconditional_elimination_left.html b/docs/build/biconditional_elimination_left.html
diff --git a/docs/build/biconditional_elimination_right.html b/docs/build/biconditional_elimination_right.html
diff --git a/docs/build/biconditional_introduction.html b/docs/build/biconditional_introduction.html
diff --git a/docs/build/conjunction_elimination_left.html b/docs/build/conjunction_elimination_left.html
diff --git a/docs/build/conjunction_elimination_right.html b/docs/build/conjunction_elimination_right.html
diff --git a/docs/build/double_negation_elimination.html b/docs/build/double_negation_elimination.html
diff --git a/docs/build/elimination_rule.html b/docs/build/elimination_rule.html
diff --git a/docs/build/introduction_rule.html b/docs/build/introduction_rule.html
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		biconditional-elimination-left
		===============================
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		biconditional-elimination-right
		===============================
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		biconditional-introduction
		===============================
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		conjunction-elimination-left
		===============================
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		conjunction-elimination-right
		===============================
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		double-negation-elimination
		===============================