Document judgements and reasonings in Fitch sample languages.
This commit is contained in:
Fedor Isakov
parent
54165ad367
commit
b7648ef5c3
|
|
@ -40,6 +40,9 @@
|
|||
<concept id="1080736578640" name="jetbrains.mps.lang.editor.structure.BaseEditorComponent" flags="ig" index="2wURMF">
|
||||
<child id="1080736633877" name="cellModel" index="2wV5jI" />
|
||||
</concept>
|
||||
<concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
|
||||
<child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
|
||||
</concept>
|
||||
<concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
|
||||
<reference id="1078939183255" name="editorComponent" index="PMmxG" />
|
||||
</concept>
|
||||
|
|
@ -81,6 +84,9 @@
|
|||
<concept id="1225900081164" name="jetbrains.mps.lang.editor.structure.CellModel_ReadOnlyModelAccessor" flags="sg" stub="3708815482283559694" index="1HlG4h">
|
||||
<child id="1225900141900" name="modelAccessor" index="1HlULh" />
|
||||
</concept>
|
||||
<concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
|
||||
<reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
|
||||
</concept>
|
||||
<concept id="1176717841777" name="jetbrains.mps.lang.editor.structure.QueryFunction_ModelAccess_Getter" flags="in" index="3TQlhw" />
|
||||
<concept id="1166049232041" name="jetbrains.mps.lang.editor.structure.AbstractComponent" flags="ng" index="1XWOmA">
|
||||
<reference id="1166049300910" name="conceptDeclaration" index="1XX52x" />
|
||||
|
|
@ -117,6 +123,9 @@
|
|||
<concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
|
||||
<property id="1193676396447" name="virtualPackage" index="3GE5qa" />
|
||||
</concept>
|
||||
<concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
|
||||
<property id="1169194664001" name="name" index="TrG5h" />
|
||||
</concept>
|
||||
</language>
|
||||
</registry>
|
||||
<node concept="24kQdi" id="3w0n0hzkN7k">
|
||||
|
|
@ -370,5 +379,49 @@
|
|||
<node concept="l2Vlx" id="$u9BK_zdQp" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW88l0">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="EqualityElim_DOC" />
|
||||
<ref role="1XX52x" to="yhz9:3w0n0hzkQ4j" resolve="EqualityElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW88l4" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW88lb" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Equality Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88le" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW88lh" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for equality relation." />
|
||||
<node concept="Vb9p2" id="4h0MmDW88ll" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88ln" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have two bases (premises) : PREMISE and an equality of the form (LEFT = RIGHT)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW88X5" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88X7" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must match PREMISE after consistently replacing LEFT with RIGHT (or the other way around)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW88Xg" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88Xi" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW88WY" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Replacement must be substitutable for the term being replaced." />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88Xt" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW88XD" role="3EZMnx">
|
||||
<property role="3F0ifm" value="The following quotation describes what it means for a term to be free for a variable:" />
|
||||
<node concept="Vb9p2" id="4h0MmDW88Yj" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88XQ" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" "a term t is free for a variable x in a sentence s if and only if" />
|
||||
<node concept="Vb9p2" id="4h0MmDW88Yl" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88Y4" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" no free occurrence of x occurs within the scope of a quantifier of some variable in t"" />
|
||||
<node concept="Vb9p2" id="4h0MmDW88Yn" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW88l7" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW88l2" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -63,6 +63,9 @@
|
|||
<child id="1638911550608610281" name="executeFunction" index="IWgqQ" />
|
||||
<child id="5692353713941573325" name="textFunction" index="1hCUd6" />
|
||||
</concept>
|
||||
<concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
|
||||
<child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
|
||||
</concept>
|
||||
<concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
|
||||
<reference id="1078939183255" name="editorComponent" index="PMmxG" />
|
||||
</concept>
|
||||
|
|
@ -70,6 +73,9 @@
|
|||
<concept id="4323500428136740385" name="jetbrains.mps.lang.editor.structure.CellIdReferenceSelector" flags="ng" index="2TlHUq">
|
||||
<reference id="4323500428136742952" name="id" index="2TlMyj" />
|
||||
</concept>
|
||||
<concept id="1186403751766" name="jetbrains.mps.lang.editor.structure.FontStyleStyleClassItem" flags="ln" index="Vb9p2">
|
||||
<property id="1186403771423" name="style" index="Vbekb" />
|
||||
</concept>
|
||||
<concept id="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
|
||||
<property id="1186414551515" name="flag" index="VOm3f" />
|
||||
</concept>
|
||||
|
|
@ -143,6 +149,9 @@
|
|||
<child id="1948540814633499358" name="editorContext" index="lBI5i" />
|
||||
<child id="1948540814635895774" name="cellSelector" index="lGT1i" />
|
||||
</concept>
|
||||
<concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
|
||||
<reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
|
||||
</concept>
|
||||
<concept id="1161622981231" name="jetbrains.mps.lang.editor.structure.ConceptFunctionParameter_editorContext" flags="nn" index="1Q80Hx" />
|
||||
<concept id="7980428675268276156" name="jetbrains.mps.lang.editor.structure.TransformationMenuSection" flags="ng" index="1Qtc8_">
|
||||
<child id="7980428675268276157" name="locations" index="1Qtc8$" />
|
||||
|
|
@ -991,5 +1000,162 @@
|
|||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="aqKnT" to="bw37:3w0n0hzg5do" resolve="HerbrandProof" />
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8b4o">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="ExistsElim_DOC" />
|
||||
<ref role="1XX52x" to="bw37:Vo$tzLEGtG" resolve="ExistsElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8b4s" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8b4z" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Existential Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8b4A" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8b4D" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for existential quantifier (∃)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8b4H" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8b4J" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have two bases (premises) : " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8b4R" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8b4T" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" first of the form (∃ X. SENTENCE)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8b4U" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8b53" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" and second of the form (∀ Y. UNI_SENTENCE => CONCLUSION)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8b54" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8bOi" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where CONCLUSION is the judgement's conclusion." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8bOu" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8bOw" role="3EZMnx">
|
||||
<property role="3F0ifm" value="SENTENCE must match UNI_SENTENCE after consistently replacing X with Y." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8bPf" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8bOI" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8bOX" role="3EZMnx">
|
||||
<property role="3F0ifm" value="The variable must not occurr free in the conclusion." />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8b4v" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8b4q" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8gM_">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="ExistsIntro_DOC" />
|
||||
<ref role="1XX52x" to="bw37:Vo$tzLEGtF" resolve="ExistsIntro" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8gMD" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8gMK" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Existential Introduction" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8gMN" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8gMQ" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Constructor for existential quantifier (∃)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8gMU" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8gMW" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have one arbitrary basis (premise) : PREMISE." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8gN2" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8gN4" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must match (∃ X. SENTENCE)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8gNl" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8gNc" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where SENTENCE must match PREMISE after consistently replacing X with a fresh variable." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8gNn" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8gMG" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8gMB" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8lQU">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="ForallElim_DOC" />
|
||||
<ref role="1XX52x" to="bw37:Vo$tzLEGtE" resolve="ForallElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8lQY" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8lX_" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Universal Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8lXC" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8lXF" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for universal quantifier (∀)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8lXJ" role="3F10Kt">
|
||||
<property role="Vbekb" value="PLAIN" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8lXL" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have one basis (premise) : a universal sentence (∀ X.SENTENCE)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8lXY" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8lY0" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where SENTENCE must match the conclusion after consistently replacing X with a fresh variable." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8lY9" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8lXR" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW88XD" role="3EZMnx">
|
||||
<property role="3F0ifm" value="The following quotation describes what it means for a term to be free for a variable:" />
|
||||
<node concept="Vb9p2" id="4h0MmDW88Yj" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88XQ" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" "a term t is free for a variable x in a sentence s if and only if" />
|
||||
<node concept="Vb9p2" id="4h0MmDW88Yl" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW88Y4" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" no free occurrence of x occurs within the scope of a quantifier of some variable in t"" />
|
||||
<node concept="Vb9p2" id="4h0MmDW88Yn" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8lYb" role="3EZMnx" />
|
||||
<node concept="2iRkQZ" id="4h0MmDW8lR1" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8lQW" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8lZG">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="ForallIntro_DOC" />
|
||||
<ref role="1XX52x" to="bw37:Vo$tzLEGtD" resolve="ForallIntro" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8lZK" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8lZR" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Universal Introduction" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8lZU" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8lZX" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Constructor for universal quantifier (∀). " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8m0$" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8m0l" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have one basis (premise) PREMISE." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8m1v" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8m0M" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must be of the form (∀ X.PREMISE)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8m1x" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8m0T" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8m1k" role="3EZMnx">
|
||||
<property role="3F0ifm" value="The following quote explains what it means for the quantified variable to be valid:" />
|
||||
<node concept="Vb9p2" id="4h0MmDW8m1B" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8m11" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" "if the variable being quantified appears in the sentence being quantified," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8m1z" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8m1a" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" it must not appear free in any active assumption"." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8m1_" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8lZN" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8lZI" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -67,9 +67,13 @@
|
|||
<child id="1638911550608610281" name="executeFunction" index="IWgqQ" />
|
||||
<child id="5692353713941573325" name="textFunction" index="1hCUd6" />
|
||||
</concept>
|
||||
<concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
|
||||
<child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
|
||||
</concept>
|
||||
<concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
|
||||
<reference id="1078939183255" name="editorComponent" index="PMmxG" />
|
||||
</concept>
|
||||
<concept id="1186403751766" name="jetbrains.mps.lang.editor.structure.FontStyleStyleClassItem" flags="ln" index="Vb9p2" />
|
||||
<concept id="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
|
||||
<property id="1186414551515" name="flag" index="VOm3f" />
|
||||
</concept>
|
||||
|
|
@ -132,6 +136,9 @@
|
|||
<concept id="5624877018228264944" name="jetbrains.mps.lang.editor.structure.TransformationMenuContribution" flags="ng" index="3INDKC">
|
||||
<child id="6718020819489956031" name="menuReference" index="AmTjC" />
|
||||
</concept>
|
||||
<concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
|
||||
<reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
|
||||
</concept>
|
||||
<concept id="1161622981231" name="jetbrains.mps.lang.editor.structure.ConceptFunctionParameter_editorContext" flags="nn" index="1Q80Hx" />
|
||||
<concept id="7980428675268276156" name="jetbrains.mps.lang.editor.structure.TransformationMenuSection" flags="ng" index="1Qtc8_">
|
||||
<child id="7980428675268276157" name="locations" index="1Qtc8$" />
|
||||
|
|
@ -1397,5 +1404,315 @@
|
|||
<property role="3GE5qa" value="proof" />
|
||||
<ref role="aqKnT" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW7NlC">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="AndElim_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3UTz" resolve="AndElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW7NlG" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW7NlN" role="3EZMnx">
|
||||
<property role="3F0ifm" value="And Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW7NlQ" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW7NlT" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for And (&)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW7NlX" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW7Os5" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Requires one basis (premise), which must have a form of conjunction." />
|
||||
<node concept="Vb9p2" id="4h0MmDW7Osb" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW83hg" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must match one of the conjunction members." />
|
||||
<node concept="Vb9p2" id="4h0MmDW83ho" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW7NlJ" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW7NlE" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW83hN">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="AndIntro_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3URE" resolve="AndIntro" />
|
||||
<node concept="3EZMnI" id="4h0MmDW83hR" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW83hY" role="3EZMnx">
|
||||
<property role="3F0ifm" value="And Introduction" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW83i1" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW83i4" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Constructor for And (&)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW83i8" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW83ia" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have two bases (premises) : A and B." />
|
||||
<node concept="Vb9p2" id="4h0MmDW83ig" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW83ii" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must be a conjunction of its bases : (A & B)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW83iq" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW83hU" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW83hP" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8yNo">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="IfElim_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3ZJm" resolve="IfElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8yNs" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8yNz" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Implication Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yNA" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8yND" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for implication (=>) (modus ponens). " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8yNM" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yNH" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have two bases (premises) :•" />
|
||||
<node concept="Vb9p2" id="4h0MmDW8yO8" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yNO" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" first of the form (SENTENCE => CONCLUSION)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8yNV" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yNX" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" and second SENTENCE," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8yO6" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z3P" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where CONCLUSION is the judgement's conslusion." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z41" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8yNv" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8yNq" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8yP0">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="IfIntro_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3ZJ9" resolve="IfIntro" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8yP4" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8yPb" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Implication Introduction" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yPe" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8yPh" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Constructor for implication (=>)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8yPl" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yVE" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have one basis (premise) which is an assumption in the preceding subproof." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8yVR" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yVK" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must be be of the form (ASSUMPTION => LAST)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8yVT" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8Ooi" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where ASSUMPTION is the assumption in the preceding subproof," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8OoB" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8Oos" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" and LAST is the last judgement in the same subproof." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8OoD" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8yP7" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8yP2" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8yWk">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="IffElim_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3ZJo" resolve="IffElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8yWo" role="2wV5jI">
|
||||
<node concept="2iRkQZ" id="4h0MmDW8yWr" role="2iSdaV" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8yWv" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Biconditional Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yWx" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8z1a" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for Biconditional (<=>). " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z1i" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8yW$" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have one basis (premise) of the form (A <=> B) or (B <=> A). " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z0e" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z09" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must be of the form (A => B). " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z0g" role="3F10Kt" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8yWm" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8z0F">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="IffIntro_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3ZJn" resolve="IffIntro" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8z0J" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8z0Q" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Biconditional Introduction" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z13" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8z16" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Constructor for Biconditinoal (<=>)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z1k" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z1m" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have two bases (premises) of the form (A => B) and (B => A)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z1z" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z1s" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must be of the form (A <=> B)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z1_" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8z0M" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8z0H" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8z20">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="NotElim_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3ZJ8" resolve="NotElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8z24" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8z2b" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Negation Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z2e" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8z2h" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for negation (~)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z2l" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z2n" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have one basis (premise) of the form (~~CONCLUSION)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z2t" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z43" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where CONCLUSION is the judgement's conclusion." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z4b" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8z27" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8z22" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8z2S">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="NotIntro_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3UTA" resolve="NotIntro" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8z2W" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8z33" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Negation Introduction" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z36" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8z39" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Constructor for negation (~)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z3d" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z3f" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have two bases (premises) : " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z3H" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z3l" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" one of the form (SENTENCE => A)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z3J" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z3s" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" and another of the form (SENTENCE => ~A)" />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z3L" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z3$" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must be of the form ~SENTENCE." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z3N" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8z2Z" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8z2U" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8z4A">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="OrElim_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3UT_" resolve="OrElim" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8z4E" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8z4L" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Or Elimination" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z4O" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8z4R" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Eliminator for Or (|)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z50" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8z52" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have three bases (premises): " />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$bP" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$bf" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" first of the form (A => CONCLUSION)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$bR" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$bn" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" second of the form (B => CONCLUSION)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$bT" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$bw" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" and third of the form (A | B) or (B | A)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$bV" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$bE" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where CONCLUSION is the judgement's conclusion." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$bX" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8z4H" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8z4C" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8$cA">
|
||||
<property role="3GE5qa" value="proof.rule" />
|
||||
<property role="TrG5h" value="OrIntro_DOC" />
|
||||
<ref role="1XX52x" to="27wh:3JXBM6C3UT$" resolve="OrIntro" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8$cE" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8$cL" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Or Introduction" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$cO" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8$cR" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Constructor for Or (|)." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$cV" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$cX" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Must have one basis (premise) : PREMISE." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$kk" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$k5" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Conclusion must be of the form (SENTENCE | PREMISE) or (PREMISE | SENTENCE)," />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$km" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$kc" role="3EZMnx">
|
||||
<property role="3F0ifm" value=" where SENTENCE is any sentence." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8$ko" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8$cH" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8$cC" role="1PM95z">
|
||||
<ref role="1PE7su" to="8v9h:4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@
|
|||
<child id="414384289274416996" name="parts" index="3ft7WO" />
|
||||
</concept>
|
||||
<concept id="1071666914219" name="jetbrains.mps.lang.editor.structure.ConceptEditorDeclaration" flags="ig" index="24kQdi">
|
||||
<child id="1078153129734" name="inspectedCellModel" index="6VMZX" />
|
||||
<child id="2597348684684069742" name="contextHints" index="CpUAK" />
|
||||
</concept>
|
||||
<concept id="6822301196700715228" name="jetbrains.mps.lang.editor.structure.ConceptEditorHintDeclarationReference" flags="ig" index="2aJ2om">
|
||||
|
|
@ -33,6 +34,7 @@
|
|||
<concept id="1196434649611" name="jetbrains.mps.lang.editor.structure.SubstituteMenu_SimpleString" flags="ng" index="2h3Zct">
|
||||
<property id="1196434851095" name="text" index="2h4Kg1" />
|
||||
</concept>
|
||||
<concept id="1106270571710" name="jetbrains.mps.lang.editor.structure.CellLayout_Vertical" flags="nn" index="2iRkQZ" />
|
||||
<concept id="1237303669825" name="jetbrains.mps.lang.editor.structure.CellLayout_Indent" flags="nn" index="l2Vlx" />
|
||||
<concept id="1237307900041" name="jetbrains.mps.lang.editor.structure.IndentLayoutIndentStyleClassItem" flags="ln" index="lj46D" />
|
||||
<concept id="1237308012275" name="jetbrains.mps.lang.editor.structure.IndentLayoutNewLineStyleClassItem" flags="ln" index="ljvvj" />
|
||||
|
|
@ -61,6 +63,9 @@
|
|||
<child id="8371900013785948365" name="parameterQuery" index="2$S_pT" />
|
||||
</concept>
|
||||
<concept id="1638911550608571617" name="jetbrains.mps.lang.editor.structure.TransformationMenu_Default" flags="ng" index="IW6AY" />
|
||||
<concept id="1078938745671" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclaration" flags="ig" index="PKFIW">
|
||||
<child id="7033942394258392116" name="overridenEditorComponent" index="1PM95z" />
|
||||
</concept>
|
||||
<concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
|
||||
<reference id="1078939183255" name="editorComponent" index="PMmxG" />
|
||||
</concept>
|
||||
|
|
@ -123,6 +128,9 @@
|
|||
<concept id="1225900081164" name="jetbrains.mps.lang.editor.structure.CellModel_ReadOnlyModelAccessor" flags="sg" stub="3708815482283559694" index="1HlG4h">
|
||||
<child id="1225900141900" name="modelAccessor" index="1HlULh" />
|
||||
</concept>
|
||||
<concept id="7033942394256351208" name="jetbrains.mps.lang.editor.structure.EditorComponentDeclarationReference" flags="ng" index="1PE4EZ">
|
||||
<reference id="7033942394256351817" name="editorComponent" index="1PE7su" />
|
||||
</concept>
|
||||
<concept id="1176717841777" name="jetbrains.mps.lang.editor.structure.QueryFunction_ModelAccess_Getter" flags="in" index="3TQlhw" />
|
||||
<concept id="2722384699544370949" name="jetbrains.mps.lang.editor.structure.SubstituteMenuPart_Placeholder" flags="ng" index="3VyMlK" />
|
||||
<concept id="4307758654696938365" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_RefPresentation" flags="ig" index="1WAQ3h" />
|
||||
|
|
@ -310,6 +318,9 @@
|
|||
</node>
|
||||
<node concept="l2Vlx" id="3JXBM6C3MQ8" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="PMmxH" id="4h0MmDW7Yu1" role="6VMZX">
|
||||
<ref role="PMmxG" node="4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="3JXBM6C3Pwn">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
|
|
@ -320,6 +331,9 @@
|
|||
</node>
|
||||
<node concept="l2Vlx" id="3JXBM6C3Pws" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="PMmxH" id="4h0MmDW7Nkt" role="6VMZX">
|
||||
<ref role="PMmxG" node="4h0MmDW7Nk2" resolve="Assumption_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="3JXBM6C3UQE">
|
||||
<property role="3GE5qa" value="proof" />
|
||||
|
|
@ -629,6 +643,9 @@
|
|||
<node concept="2aJ2om" id="$u9BK_zG8W" role="CpUAK">
|
||||
<ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
|
||||
</node>
|
||||
<node concept="PMmxH" id="4h0MmDW7Nkv" role="6VMZX">
|
||||
<ref role="PMmxG" node="4h0MmDW7Nk2" resolve="Assumption_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="$u9BK_zGGT">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
|
|
@ -681,6 +698,9 @@
|
|||
<node concept="2aJ2om" id="$u9BK_zGGX" role="CpUAK">
|
||||
<ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
|
||||
</node>
|
||||
<node concept="PMmxH" id="4h0MmDW7YtZ" role="6VMZX">
|
||||
<ref role="PMmxG" node="4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="$u9BK__JRm">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
|
|
@ -691,6 +711,9 @@
|
|||
<ref role="1NtTu8" to="jfgh:2aBGSFggvpT" resolve="conclusion" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PMmxH" id="4h0MmDW7E1K" role="6VMZX">
|
||||
<ref role="PMmxG" node="4h0MmDW7E1r" resolve="Premise_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="$u9BK__JRu">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
|
|
@ -705,6 +728,9 @@
|
|||
<node concept="2aJ2om" id="$u9BK__JRw" role="CpUAK">
|
||||
<ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
|
||||
</node>
|
||||
<node concept="PMmxH" id="4h0MmDW7E1M" role="6VMZX">
|
||||
<ref role="PMmxG" node="4h0MmDW7E1r" resolve="Premise_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="24kQdi" id="$u9BK__JR_">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
|
|
@ -1004,5 +1030,72 @@
|
|||
<node concept="IW6AY" id="2DPo4JTQI2h">
|
||||
<ref role="aqKnT" to="jfgh:4LBPYGV4cY1" resolve="Sentence" />
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW7E1r">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
<property role="TrG5h" value="Premise_DOC" />
|
||||
<ref role="1XX52x" to="jfgh:$u9BK__JRe" resolve="Premise" />
|
||||
<node concept="3EZMnI" id="4h0MmDW7E1t" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW7E1$" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Premise" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW7IEj" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW7E1B" role="3EZMnx">
|
||||
<property role="3F0ifm" value="A sentence that serves as an input to the proof. Must be on top level. Doesn't require a proof." />
|
||||
<node concept="Vb9p2" id="4h0MmDW7IEh" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW7E1w" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW7Nk2">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
<property role="TrG5h" value="Assumption_DOC" />
|
||||
<ref role="1XX52x" to="jfgh:3JXBM6C3Pwi" resolve="Assumption" />
|
||||
<node concept="3EZMnI" id="4h0MmDW7Nk4" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW7Nkb" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Assumption" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW7Nke" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW7Nkh" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Introduce assumption. Starts a new subproof. " />
|
||||
<node concept="Vb9p2" id="4h0MmDW7Nkl" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW7Nk7" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW7NkU">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
<property role="TrG5h" value="Judgement_DOC" />
|
||||
<ref role="1XX52x" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
|
||||
<node concept="3EZMnI" id="4h0MmDW7NkW" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW7Nl3" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Judgement" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW7Nl6" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW7Nl9" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Judgement is an act of making a conclusion." />
|
||||
<node concept="Vb9p2" id="4h0MmDW7Nld" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW7NkZ" role="2iSdaV" />
|
||||
</node>
|
||||
</node>
|
||||
<node concept="PKFIW" id="4h0MmDW8$kN">
|
||||
<property role="3GE5qa" value="proof.reasoning" />
|
||||
<property role="TrG5h" value="Reiteration_DOC" />
|
||||
<ref role="1XX52x" to="jfgh:5jVx7S1Yau5" resolve="Reiteration" />
|
||||
<node concept="3EZMnI" id="4h0MmDW8$kR" role="2wV5jI">
|
||||
<node concept="3F0ifn" id="4h0MmDW8$kY" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Reiteration" />
|
||||
</node>
|
||||
<node concept="3F0ifn" id="4h0MmDW8$l1" role="3EZMnx" />
|
||||
<node concept="3F0ifn" id="4h0MmDW8$l4" role="3EZMnx">
|
||||
<property role="3F0ifm" value="Allows to reuse a previous assumption or a premise." />
|
||||
<node concept="Vb9p2" id="4h0MmDW8z3H" role="3F10Kt" />
|
||||
</node>
|
||||
<node concept="2iRkQZ" id="4h0MmDW8$kU" role="2iSdaV" />
|
||||
</node>
|
||||
<node concept="1PE4EZ" id="4h0MmDW8$kP" role="1PM95z">
|
||||
<ref role="1PE7su" node="4h0MmDW7NkU" resolve="Judgement_DOC" />
|
||||
</node>
|
||||
</node>
|
||||
</model>
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue