natas_hw
/
mps-coderules
mirror of https://github.com/JetBrains/mps-coderules
0
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Implementation of Herbrand logic, an example.

This commit is contained in:
Fedor Isakov 2018-01-15 17:56:18 +01:00
parent 848df81dd4
commit 25d0238155
8 changed files with 4177 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

237
samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.herbrand.mps
View File

@ -4,34 +4,40 @@
<languages>
<use id="06b7c5c7-e359-4f4b-a581-5d0c9323af39" name="jetbrains.mps.fitch" version="1" />
<use id="748b3ba1-2791-4ee8-b985-a5598baa7112" name="jetbrains.mps.logic.herbrand" version="0" />
<use id="ec79e64d-4cbb-4f6c-b7b7-108dd125aba6" name="jetbrains.mps.logic.propositional" version="0" />
</languages>
<imports />
<registry>
<language id="ec79e64d-4cbb-4f6c-b7b7-108dd125aba6" name="jetbrains.mps.logic.propositional">
<concept id="4322786184247881316" name="jetbrains.mps.logic.propositional.structure.OrIntro" flags="ng" index="2jWz55" />
<concept id="4322786184247817766" name="jetbrains.mps.logic.propositional.structure.Or" flags="ng" index="2jWM$7">
<child id="4322786184247817796" name="disjunct" index="2jWM__" />
<concept id="4322786184247901129" name="jetbrains.mps.logic.propositional.structure.IfIntro" flags="ng" index="2jWAjC" />
<concept id="4322786184247817809" name="jetbrains.mps.logic.propositional.structure.If" flags="ng" index="2jWM_K">
<child id="4322786184247817810" name="antecedent" index="2jWM_N" />
<child id="4322786184247817812" name="consequent" index="2jWM_P" />
</concept>
</language>
<language id="06b7c5c7-e359-4f4b-a581-5d0c9323af39" name="jetbrains.mps.fitch">
<concept id="4322786184247881124" name="jetbrains.mps.fitch.structure.SubProof" flags="ng" index="2jWza5">
<child id="4322786184247881125" name="content" index="2jWza4" />
</concept>
<concept id="4322786184247859218" name="jetbrains.mps.fitch.structure.Assumption" flags="ng" index="2jWGsN" />
<concept id="4322786184247854968" name="jetbrains.mps.fitch.structure.Reasoning" flags="ng" index="2jWHxp">
<child id="2497161927181071993" name="conclusion" index="3MT$nN" />
</concept>
<concept id="4322786184247818020" name="jetbrains.mps.fitch.structure.Proof" flags="ng" index="2jWMw5">
<property id="2994859399702197792" name="description" index="26WHrx" />
<child id="4322786184248036774" name="content" index="2jVTa7" />
<child id="657004910291159451" name="goal" index="GyqZB" />
</concept>
<concept id="4322786184247818022" name="jetbrains.mps.fitch.structure.Judgement" flags="ng" index="2jWMw7">
<child id="4322786184247848320" name="premise" index="2jWFax" />
<child id="4322786184247848320" name="basis" index="2jWFax" />
</concept>
<concept id="4322786184247818035" name="jetbrains.mps.fitch.structure.Basis" flags="ng" index="2jWMwi">
<concept id="4322786184247818035" name="jetbrains.mps.fitch.structure.Reference" flags="ng" index="2jWMwi">
<reference id="4322786184247818157" name="reasoning" index="2jWMyc" />
</concept>
<concept id="657004910291123662" name="jetbrains.mps.fitch.structure.Premise" flags="ng" index="GydIM" />
<concept id="657004910291159432" name="jetbrains.mps.fitch.structure.Goal" flags="ng" index="GyqZO">
<child id="657004910291159433" name="sentence" index="GyqZP" />
</concept>
<concept id="4035326440038975469" name="jetbrains.mps.fitch.structure.AbstractProof" flags="ng" index="1rgTJD">
<property id="2994859399702197792" name="description" index="26WHrx" />
<child id="4322786184248036774" name="content" index="2jVTa7" />
<child id="657004910291159451" name="goal" index="GyqZB" />
</concept>
</language>
<language id="748b3ba1-2791-4ee8-b985-a5598baa7112" name="jetbrains.mps.logic.herbrand">
<concept id="3059457401299011405" name="jetbrains.mps.logic.herbrand.structure.Forall" flags="ng" index="3jEQs6">
@ -45,8 +51,11 @@
<concept id="3059457401299011425" name="jetbrains.mps.logic.herbrand.structure.Relation" flags="ng" index="3jEQsE">
<child id="3059457401299011435" name="member" index="3jEQsw" />
</concept>
<concept id="3059457401299011374" name="jetbrains.mps.logic.herbrand.structure.Object" flags="ng" index="3jEQt_" />
<concept id="3059457401299011378" name="jetbrains.mps.logic.herbrand.structure.Variable" flags="ng" index="3jEQtT" />
<concept id="4035326440038749016" name="jetbrains.mps.logic.herbrand.structure.HerbrandProof" flags="ng" index="1rg0Xs" />
<concept id="1069765272453957481" name="jetbrains.mps.logic.herbrand.structure.ForallIntro" flags="ng" index="3Zs_qL" />
<concept id="1069765272453957482" name="jetbrains.mps.logic.herbrand.structure.ForallElim" flags="ng" index="3Zs_qM" />
<concept id="1069765272453957484" name="jetbrains.mps.logic.herbrand.structure.ExistsElim" flags="ng" index="3Zs_qO" />
</language>
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
<concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
@ -54,54 +63,180 @@
</concept>
</language>
</registry>
<node concept="2jWMw5" id="2DPo4JTSM5F">
<property role="TrG5h" value="Test1" />
<property role="26WHrx" value="Proove EX.p(X) given AX.p(X)" />
<node concept="GyqZO" id="Vo$tzLD0uS" role="GyqZB">
<node concept="3jEQso" id="Vo$tzLD0uW" role="GyqZP">
<node concept="3jEQtT" id="Vo$tzLD0uY" role="3jEQsj">
<node concept="1rg0Xs" id="3w0n0hzkMd2">
<property role="TrG5h" value="Example" />
<property role="26WHrx" value="Proove AX.(EY.p(X,Y) =&gt; q(X)) given AX.AY.(p(X,Y) =&gt; q(X))" />
<node concept="GydIM" id="3w0n0hzkMdq" role="2jVTa7">
<node concept="3jEQs6" id="3w0n0hzkMdr" role="3MT$nN">
<node concept="3jEQtT" id="3w0n0hzkMds" role="3jEQsg">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQsE" id="Vo$tzLD0v7" role="3jEQst">
<property role="TrG5h" value="p" />
<node concept="3jEQtT" id="Vo$tzLD0vb" role="3jEQsw">
<property role="TrG5h" value="X" />
<node concept="3jEQs6" id="3w0n0hzkMdt" role="3jEQsn">
<node concept="3jEQtT" id="3w0n0hzkMdu" role="3jEQsg">
<property role="TrG5h" value="Y" />
</node>
<node concept="2jWM_K" id="3w0n0hzkMdv" role="3jEQsn">
<node concept="3jEQsE" id="3w0n0hzkMdw" role="2jWM_N">
<property role="TrG5h" value="p" />
<node concept="3jEQtT" id="3w0n0hzkMdx" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQtT" id="3w0n0hzkMdy" role="3jEQsw">
<property role="TrG5h" value="Y" />
</node>
</node>
<node concept="3jEQsE" id="3w0n0hzkMdz" role="2jWM_P">
<property role="TrG5h" value="q" />
<node concept="3jEQtT" id="3w0n0hzkMd$" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
</node>
</node>
</node>
</node>
</node>
<node concept="GydIM" id="Vo$tzLD32O" role="2jVTa7">
<node concept="3jEQs6" id="Vo$tzLD32S" role="3MT$nN">
<node concept="3jEQtT" id="Vo$tzLD32U" role="3jEQsg">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQsE" id="Vo$tzLD333" role="3jEQsn">
<property role="TrG5h" value="p" />
<node concept="3jEQtT" id="Vo$tzLD335" role="3jEQsw">
<property role="TrG5h" value="X" />
<node concept="2jWza5" id="3w0n0hzkMd_" role="2jVTa7">
<node concept="2jWGsN" id="3w0n0hzkMdA" role="2jWza4">
<node concept="3jEQso" id="3w0n0hzkMdB" role="3MT$nN">
<node concept="3jEQtT" id="3w0n0hzkMdC" role="3jEQsj">
<property role="TrG5h" value="Y" />
</node>
</node>
</node>
</node>
<node concept="2jWz55" id="Vo$tzLD33x" role="2jVTa7">
<node concept="2jWMwi" id="Vo$tzLD33I" role="2jWFax">
<ref role="2jWMyc" node="Vo$tzLD32O" />
</node>
<node concept="2jWM$7" id="Vo$tzLD33T" role="3MT$nN">
<node concept="3jEQsE" id="Vo$tzLD33O" role="2jWM__">
<property role="TrG5h" value="q" />
<node concept="3jEQtT" id="Vo$tzLD33Q" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
</node>
<node concept="3jEQs6" id="Vo$tzLD342" role="2jWM__">
<node concept="3jEQtT" id="Vo$tzLD344" role="3jEQsg">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQsE" id="Vo$tzLDATB" role="3jEQsn">
<node concept="3jEQsE" id="3w0n0hzkMdD" role="3jEQst">
<property role="TrG5h" value="p" />
<node concept="3jEQt_" id="Vo$tzLDDC2" role="3jEQsw">
<property role="TrG5h" value="fun" />
<node concept="3jEQtT" id="3w0n0hzkMdE" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQtT" id="3w0n0hzkMdF" role="3jEQsw">
<property role="TrG5h" value="Y" />
</node>
</node>
</node>
</node>
<node concept="3Zs_qM" id="3w0n0hzkMdG" role="2jWza4">
<node concept="2jWMwi" id="3w0n0hzkMdH" role="2jWFax">
<ref role="2jWMyc" node="3w0n0hzkMdq" />
</node>
<node concept="3jEQs6" id="3w0n0hzkMdI" role="3MT$nN">
<node concept="3jEQtT" id="3w0n0hzkMdJ" role="3jEQsg">
<property role="TrG5h" value="Y" />
</node>
<node concept="2jWM_K" id="3w0n0hzkMdK" role="3jEQsn">
<node concept="3jEQsE" id="3w0n0hzkMdL" role="2jWM_N">
<property role="TrG5h" value="p" />
<node concept="3jEQtT" id="3w0n0hzkMdM" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQtT" id="3w0n0hzkMdN" role="3jEQsw">
<property role="TrG5h" value="Y" />
</node>
</node>
<node concept="3jEQsE" id="3w0n0hzkMdO" role="2jWM_P">
<property role="TrG5h" value="q" />
<node concept="3jEQtT" id="3w0n0hzkMdP" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
</node>
</node>
</node>
</node>
<node concept="3Zs_qO" id="3w0n0hzkMdQ" role="2jWza4">
<node concept="2jWMwi" id="3w0n0hzkMdR" role="2jWFax">
<ref role="2jWMyc" node="3w0n0hzkMdA" />
</node>
<node concept="2jWMwi" id="3w0n0hzkMdS" role="2jWFax">
<ref role="2jWMyc" node="3w0n0hzkMdG" />
</node>
<node concept="3jEQsE" id="3w0n0hzkMdT" role="3MT$nN">
<property role="TrG5h" value="q" />
<node concept="3jEQtT" id="3w0n0hzkMdU" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
</node>
</node>
</node>
<node concept="2jWAjC" id="3w0n0hzkMdV" role="2jVTa7">
<node concept="2jWMwi" id="3w0n0hzkMdW" role="2jWFax">
<ref role="2jWMyc" node="3w0n0hzkMd_" />
</node>
<node concept="2jWM_K" id="3w0n0hzkMdX" role="3MT$nN">
<node concept="3jEQsE" id="3w0n0hzkMdY" role="2jWM_P">
<property role="TrG5h" value="q" />
<node concept="3jEQtT" id="3w0n0hzkMdZ" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
</node>
<node concept="3jEQso" id="3w0n0hzkMe0" role="2jWM_N">
<node concept="3jEQtT" id="3w0n0hzkMe1" role="3jEQsj">
<property role="TrG5h" value="Y" />
</node>
<node concept="3jEQsE" id="3w0n0hzkMe2" role="3jEQst">
<property role="TrG5h" value="p" />
<node concept="3jEQtT" id="3w0n0hzkMe3" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQtT" id="3w0n0hzkMe4" role="3jEQsw">
<property role="TrG5h" value="Y" />
</node>
</node>
</node>
</node>
</node>
<node concept="3Zs_qL" id="3w0n0hzkMe5" role="2jVTa7">
<node concept="2jWMwi" id="3w0n0hzkMe6" role="2jWFax">
<ref role="2jWMyc" node="3w0n0hzkMdV" />
</node>
<node concept="3jEQs6" id="3w0n0hzkMe7" role="3MT$nN">
<node concept="3jEQtT" id="3w0n0hzkMe8" role="3jEQsg">
<property role="TrG5h" value="X" />
</node>
<node concept="2jWM_K" id="3w0n0hzkMe9" role="3jEQsn">
<node concept="3jEQsE" id="3w0n0hzkMea" role="2jWM_P">
<property role="TrG5h" value="q" />
<node concept="3jEQtT" id="3w0n0hzkMeb" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
</node>
<node concept="3jEQso" id="3w0n0hzkMec" role="2jWM_N">
<node concept="3jEQtT" id="3w0n0hzkMed" role="3jEQsj">
<property role="TrG5h" value="Y" />
</node>
<node concept="3jEQsE" id="3w0n0hzkMee" role="3jEQst">
<property role="TrG5h" value="p" />
<node concept="3jEQtT" id="3w0n0hzkMef" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQtT" id="3w0n0hzkMeg" role="3jEQsw">
<property role="TrG5h" value="Y" />
</node>
</node>
</node>
</node>
</node>
</node>
<node concept="GyqZO" id="3w0n0hzkMd4" role="GyqZB">
<node concept="3jEQs6" id="3w0n0hzkMd5" role="GyqZP">
<node concept="3jEQtT" id="3w0n0hzkMd6" role="3jEQsg">
<property role="TrG5h" value="X" />
</node>
<node concept="2jWM_K" id="3w0n0hzkMd7" role="3jEQsn">
<node concept="3jEQsE" id="3w0n0hzkMd8" role="2jWM_P">
<property role="TrG5h" value="q" />
<node concept="3jEQtT" id="3w0n0hzkMd9" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
</node>
<node concept="3jEQso" id="3w0n0hzkMda" role="2jWM_N">
<node concept="3jEQtT" id="3w0n0hzkMdb" role="3jEQsj">
<property role="TrG5h" value="Y" />
</node>
<node concept="3jEQsE" id="3w0n0hzkMdc" role="3jEQst">
<property role="TrG5h" value="p" />
<node concept="3jEQtT" id="3w0n0hzkMdd" role="3jEQsw">
<property role="TrG5h" value="X" />
</node>
<node concept="3jEQtT" id="3w0n0hzkMde" role="3jEQsw">
<property role="TrG5h" value="Y" />
</node>
</node>
</node>
</node>

4
samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.propositional.mps
View File

@ -47,9 +47,9 @@
<child id="2497161927181071993" name="conclusion" index="3MT$nN" />
</concept>
<concept id="4322786184247818022" name="jetbrains.mps.fitch.structure.Judgement" flags="ng" index="2jWMw7">
<child id="4322786184247848320" name="premise" index="2jWFax" />
<child id="4322786184247848320" name="basis" index="2jWFax" />
</concept>
<concept id="4322786184247818035" name="jetbrains.mps.fitch.structure.Basis" flags="ng" index="2jWMwi">
<concept id="4322786184247818035" name="jetbrains.mps.fitch.structure.Reference" flags="ng" index="2jWMwi">
<reference id="4322786184247818157" name="reasoning" index="2jWMyc" />
</concept>
<concept id="657004910291123662" name="jetbrains.mps.fitch.structure.Premise" flags="ng" index="GydIM" />

4
samples/fitch/languages/jetbrains.mps.logic.herbrand/jetbrains.mps.logic.herbrand.mpl
View File

@ -51,6 +51,8 @@
<dependencies>
<dependency reexport="false">748b3ba1-2791-4ee8-b985-a5598baa7112(jetbrains.mps.logic.herbrand)</dependency>
<dependency reexport="false">daafa647-f1f7-4b0b-b096-69cd7c8408c0(jetbrains.mps.baseLanguage.regexp)</dependency>
<dependency reexport="false">06b7c5c7-e359-4f4b-a581-5d0c9323af39(jetbrains.mps.fitch)</dependency>
<dependency reexport="false">ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)</dependency>
</dependencies>
<languageVersions>
<language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="5" />
@ -87,6 +89,8 @@
<language slang="l:b83431fe-5c8f-40bc-8a36-65e25f4dd253:jetbrains.mps.lang.textGen" version="1" />
<language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" version="0" />
<language slang="l:7a5dda62-9140-4668-ab76-d5ed1746f2b2:jetbrains.mps.lang.typesystem" version="1" />
<language slang="l:c4803b19-6d89-4a3b-bf82-390769514add:jetbrains.mps.lang.typesystem2" version="7" />
<language slang="l:35320f26-77cb-4c55-be9f-a97a27770af1:jetbrains.mps.logic" version="2" />
</languageVersions>
<dependencyVersions>
<module reference="3f233e7f-b8a6-46d2-a57f-795d56775243(Annotations)" version="0" />

121
samples/fitch/languages/jetbrains.mps.logic.herbrand/models/behavior.mps
View File

@ -5,7 +5,124 @@
<use id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior" version="1" />
<devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />
</languages>
<imports />
<registry />
<imports>
<import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" />
<import index="bw37" ref="r:faa478da-573c-4c9e-99e4-b87297289505(jetbrains.mps.logic.herbrand.structure)" implicit="true" />
<import index="27wh" ref="r:459ba7ac-2a61-40fc-bcc4-f13a7956cbeb(jetbrains.mps.logic.propositional.structure)" implicit="true" />
</imports>
<registry>
<language id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior">
<concept id="1225194240794" name="jetbrains.mps.lang.behavior.structure.ConceptBehavior" flags="ng" index="13h7C7">
<reference id="1225194240799" name="concept" index="13h7C2" />
<child id="1225194240805" name="method" index="13h7CS" />
<child id="1225194240801" name="constructor" index="13h7CW" />
</concept>
<concept id="1225194413805" name="jetbrains.mps.lang.behavior.structure.ConceptConstructorDeclaration" flags="in" index="13hLZK" />
<concept id="1225194472830" name="jetbrains.mps.lang.behavior.structure.ConceptMethodDeclaration" flags="ng" index="13i0hz">
<property id="1225194472832" name="isVirtual" index="13i0it" />
<property id="1225194472834" name="isAbstract" index="13i0iv" />
<reference id="1225194472831" name="overriddenMethod" index="13i0hy" />
</concept>
</language>
<language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
<concept id="1080223426719" name="jetbrains.mps.baseLanguage.structure.OrExpression" flags="nn" index="22lmx$" />
<concept id="1197027756228" name="jetbrains.mps.baseLanguage.structure.DotExpression" flags="nn" index="2OqwBi">
<child id="1197027771414" name="operand" index="2Oq$k0" />
<child id="1197027833540" name="operation" index="2OqNvi" />
</concept>
<concept id="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
<child id="1137022507850" name="body" index="2VODD2" />
</concept>
<concept id="1070534644030" name="jetbrains.mps.baseLanguage.structure.BooleanType" flags="in" index="10P_77" />
<concept id="1068498886296" name="jetbrains.mps.baseLanguage.structure.VariableReference" flags="nn" index="37vLTw">
<reference id="1068581517664" name="variableDeclaration" index="3cqZAo" />
</concept>
<concept id="1068498886292" name="jetbrains.mps.baseLanguage.structure.ParameterDeclaration" flags="ir" index="37vLTG" />
<concept id="4972933694980447171" name="jetbrains.mps.baseLanguage.structure.BaseVariableDeclaration" flags="ng" index="19Szcq">
<child id="5680397130376446158" name="type" index="1tU5fm" />
</concept>
<concept id="1068580123132" name="jetbrains.mps.baseLanguage.structure.BaseMethodDeclaration" flags="ng" index="3clF44">
<child id="1068580123133" name="returnType" index="3clF45" />
<child id="1068580123134" name="parameter" index="3clF46" />
<child id="1068580123135" name="body" index="3clF47" />
</concept>
<concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
<child id="1068580123156" name="expression" index="3clFbG" />
</concept>
<concept id="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
<child id="1068581517665" name="statement" index="3cqZAp" />
</concept>
<concept id="1081773326031" name="jetbrains.mps.baseLanguage.structure.BinaryOperation" flags="nn" index="3uHJSO">
<child id="1081773367579" name="rightExpression" index="3uHU7w" />
<child id="1081773367580" name="leftExpression" index="3uHU7B" />
</concept>
<concept id="1178549954367" name="jetbrains.mps.baseLanguage.structure.IVisible" flags="ng" index="1B3ioH">
<child id="1178549979242" name="visibility" index="1B3o_S" />
</concept>
<concept id="1146644602865" name="jetbrains.mps.baseLanguage.structure.PublicVisibility" flags="nn" index="3Tm1VV" />
</language>
<language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
<concept id="1177026924588" name="jetbrains.mps.lang.smodel.structure.RefConcept_Reference" flags="nn" index="chp4Y">
<reference id="1177026940964" name="conceptDeclaration" index="cht4Q" />
</concept>
<concept id="1180031783296" name="jetbrains.mps.lang.smodel.structure.Concept_IsSubConceptOfOperation" flags="nn" index="2Zo12i">
<child id="1180031783297" name="conceptArgument" index="2Zo12j" />
</concept>
<concept id="6677504323281689838" name="jetbrains.mps.lang.smodel.structure.SConceptType" flags="in" index="3bZ5Sz" />
</language>
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
<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="13h7C7" id="3w0n0hzjO0D">
<property role="3GE5qa" value="proof" />
<ref role="13h7C2" to="bw37:3w0n0hzg5do" resolve="HerbrandProof" />
<node concept="13hLZK" id="3w0n0hzjO0E" role="13h7CW">
<node concept="3clFbS" id="3w0n0hzjO0F" role="2VODD2" />
</node>
<node concept="13i0hz" id="3w0n0hzjO0O" role="13h7CS">
<property role="13i0iv" value="false" />
<property role="13i0it" value="false" />
<property role="TrG5h" value="isRuleSupported" />
<ref role="13i0hy" to="qd7f:3w0n0hzjKLG" resolve="isRuleSupported" />
<node concept="3Tm1VV" id="3w0n0hzjO0R" role="1B3o_S" />
<node concept="3clFbS" id="3w0n0hzjO0U" role="3clF47">
<node concept="3clFbF" id="3w0n0hzjO1y" role="3cqZAp">
<node concept="22lmx$" id="3w0n0hzjQ4G" role="3clFbG">
<node concept="2OqwBi" id="3w0n0hzjQku" role="3uHU7w">
<node concept="37vLTw" id="3w0n0hzjQ85" role="2Oq$k0">
<ref role="3cqZAo" node="3w0n0hzjO0V" resolve="ruleConcept" />
</node>
<node concept="2Zo12i" id="3w0n0hzjQLS" role="2OqNvi">
<node concept="chp4Y" id="3w0n0hzjR29" role="2Zo12j">
<ref role="cht4Q" to="bw37:3w0n0hziLce" resolve="QuantifierRule" />
</node>
</node>
</node>
<node concept="2OqwBi" id="3w0n0hzjObN" role="3uHU7B">
<node concept="37vLTw" id="3w0n0hzjO1x" role="2Oq$k0">
<ref role="3cqZAo" node="3w0n0hzjO0V" resolve="ruleConcept" />
</node>
<node concept="2Zo12i" id="3w0n0hzjOzD" role="2OqNvi">
<node concept="chp4Y" id="3w0n0hzjODr" role="2Zo12j">
<ref role="cht4Q" to="27wh:3w0n0hziLcf" resolve="PropositionalRule" />
</node>
</node>
</node>
</node>
</node>
</node>
<node concept="37vLTG" id="3w0n0hzjO0V" role="3clF46">
<property role="TrG5h" value="ruleConcept" />
<node concept="3bZ5Sz" id="3w0n0hzjO0W" role="1tU5fm" />
</node>
<node concept="10P_77" id="3w0n0hzjO0X" role="3clF45" />
</node>
</node>
</model>

65
samples/fitch/languages/jetbrains.mps.logic.herbrand/models/constraints.mps
View File

@ -10,12 +10,21 @@
<import index="tpfp" ref="r:00000000-0000-4000-0000-011c89590519(jetbrains.mps.baseLanguage.regexp.jetbrains.mps.regexp.accessory)" />
<import index="bw37" ref="r:faa478da-573c-4c9e-99e4-b87297289505(jetbrains.mps.logic.herbrand.structure)" implicit="true" />
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" implicit="true" />
<import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" implicit="true" />
<import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" implicit="true" />
</imports>
<registry>
<language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
<concept id="1197027756228" name="jetbrains.mps.baseLanguage.structure.DotExpression" flags="nn" index="2OqwBi">
<child id="1197027771414" name="operand" index="2Oq$k0" />
<child id="1197027833540" name="operation" index="2OqNvi" />
</concept>
<concept id="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
<child id="1137022507850" name="body" index="2VODD2" />
</concept>
<concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
<child id="1068580123156" name="expression" index="3clFbG" />
</concept>
<concept id="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
<child id="1068581517665" name="statement" index="3cqZAp" />
</concept>
@ -25,8 +34,15 @@
<concept id="1068581242878" name="jetbrains.mps.baseLanguage.structure.ReturnStatement" flags="nn" index="3cpWs6">
<child id="1068581517676" name="expression" index="3cqZAk" />
</concept>
<concept id="1204053956946" name="jetbrains.mps.baseLanguage.structure.IMethodCall" flags="ng" index="1ndlxa">
<reference id="1068499141037" name="baseMethodDeclaration" index="37wK5l" />
<child id="1068499141038" name="actualArgument" index="37wK5m" />
</concept>
</language>
<language id="3f4bc5f5-c6c1-4a28-8b10-c83066ffa4a1" name="jetbrains.mps.lang.constraints">
<concept id="6702802731807351367" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_CanBeAChild" flags="in" index="9S07l" />
<concept id="1202989658459" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_parentNode" flags="nn" index="nLn13" />
<concept id="4303308395523096213" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_childConcept" flags="ng" index="2DD5aU" />
<concept id="1147467115080" name="jetbrains.mps.lang.constraints.structure.NodePropertyConstraint" flags="ng" index="EnEH3">
<reference id="1147467295099" name="applicableProperty" index="EomxK" />
<child id="1212097481299" name="propertyValidator" index="QCWH9" />
@ -34,10 +50,30 @@
<concept id="1212096972063" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_PropertyValidator" flags="in" index="QB0g5" />
<concept id="1213093968558" name="jetbrains.mps.lang.constraints.structure.ConceptConstraints" flags="ng" index="1M2fIO">
<reference id="1213093996982" name="concept" index="1M2myG" />
<child id="6702802731807737306" name="canBeChild" index="9Vyp8" />
<child id="1213098023997" name="property" index="1MhHOB" />
</concept>
<concept id="1153138554286" name="jetbrains.mps.lang.constraints.structure.ConstraintsFunctionParameter_propertyValue" flags="nn" index="1Wqviy" />
</language>
<language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
<concept id="1177026924588" name="jetbrains.mps.lang.smodel.structure.RefConcept_Reference" flags="nn" index="chp4Y">
<reference id="1177026940964" name="conceptDeclaration" index="cht4Q" />
</concept>
<concept id="1138411891628" name="jetbrains.mps.lang.smodel.structure.SNodeOperation" flags="nn" index="eCIE_">
<child id="1144104376918" name="parameter" index="1xVPHs" />
</concept>
<concept id="1179409122411" name="jetbrains.mps.lang.smodel.structure.Node_ConceptMethodCall" flags="nn" index="2qgKlT" />
<concept id="1171407110247" name="jetbrains.mps.lang.smodel.structure.Node_GetAncestorOperation" flags="nn" index="2Xjw5R" />
<concept id="1144100932627" name="jetbrains.mps.lang.smodel.structure.OperationParm_Inclusion" flags="ng" index="1xIGOp" />
<concept id="1144101972840" name="jetbrains.mps.lang.smodel.structure.OperationParm_Concept" flags="ng" index="1xMEDy">
<child id="1207343664468" name="conceptArgument" index="ri$Ld" />
</concept>
</language>
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
<concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
<property id="1193676396447" name="virtualPackage" index="3GE5qa" />
</concept>
</language>
<language id="daafa647-f1f7-4b0b-b096-69cd7c8408c0" name="jetbrains.mps.baseLanguage.regexp">
<concept id="1174482804200" name="jetbrains.mps.baseLanguage.regexp.structure.PlusRegexp" flags="ng" index="1OClNT" />
<concept id="1174485235885" name="jetbrains.mps.baseLanguage.regexp.structure.UnaryRegexp" flags="ng" index="1OLBAW">
@ -59,6 +95,7 @@
</language>
</registry>
<node concept="1M2fIO" id="2DPo4JTT5FI">
<property role="3GE5qa" value="sentence" />
<ref role="1M2myG" to="bw37:2DPo4JTRwsI" resolve="Object" />
<node concept="EnEH3" id="3JXBM6C7aaW" role="1MhHOB">
<ref role="EomxK" to="tpck:h0TrG11" resolve="name" />
@ -91,6 +128,7 @@
</node>
</node>
<node concept="1M2fIO" id="2DPo4JTTXyU">
<property role="3GE5qa" value="sentence" />
<ref role="1M2myG" to="bw37:2DPo4JTRwsM" resolve="Variable" />
<node concept="EnEH3" id="2DPo4JTTXyV" role="1MhHOB">
<ref role="EomxK" to="tpck:h0TrG11" resolve="name" />
@ -122,5 +160,32 @@
</node>
</node>
</node>
<node concept="1M2fIO" id="3w0n0hzjECi">
<property role="3GE5qa" value="proof.rule" />
<ref role="1M2myG" to="bw37:3w0n0hziLce" resolve="QuantifierRule" />
<node concept="9S07l" id="3w0n0hzjECG" role="9Vyp8">
<node concept="3clFbS" id="3w0n0hzjECH" role="2VODD2">
<node concept="3clFbF" id="3w0n0hzjEJQ" role="3cqZAp">
<node concept="2OqwBi" id="3w0n0hzjFH7" role="3clFbG">
<node concept="2OqwBi" id="3w0n0hzjEZ0" role="2Oq$k0">
<node concept="nLn13" id="3w0n0hzjEJP" role="2Oq$k0" />
<node concept="2Xjw5R" id="3w0n0hzjFfL" role="2OqNvi">
<node concept="1xMEDy" id="3w0n0hzjSnx" role="1xVPHs">
<node concept="chp4Y" id="3w0n0hzjS$2" role="ri$Ld">
<ref role="cht4Q" to="jfgh:3JXBM6C5urr" resolve="Root" />
</node>
</node>
<node concept="1xIGOp" id="3w0n0hzjSWs" role="1xVPHs" />
</node>
</node>
<node concept="2qgKlT" id="3w0n0hzjTgg" role="2OqNvi">
<ref role="37wK5l" to="qd7f:3w0n0hzjKLG" resolve="isRuleSupported" />
<node concept="2DD5aU" id="3w0n0hzjTDM" role="37wK5m" />
</node>
</node>
</node>
</node>
</node>
</node>
</model>

186
samples/fitch/languages/jetbrains.mps.logic.herbrand/models/editor.mps
View File

@ -9,6 +9,9 @@
<imports>
<import index="bw37" ref="r:faa478da-573c-4c9e-99e4-b87297289505(jetbrains.mps.logic.herbrand.structure)" />
<import index="27wh" ref="r:459ba7ac-2a61-40fc-bcc4-f13a7956cbeb(jetbrains.mps.logic.propositional.structure)" />
<import index="tpco" ref="r:00000000-0000-4000-0000-011c89590284(jetbrains.mps.lang.core.editor)" />
<import index="8v9h" ref="r:873e37f0-b045-47b9-ae9e-db79c2628975(jetbrains.mps.fitch.editor)" />
<import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" implicit="true" />
<import index="tpfp" ref="r:00000000-0000-4000-0000-011c89590519(jetbrains.mps.baseLanguage.regexp.jetbrains.mps.regexp.accessory)" implicit="true" />
</imports>
@ -20,6 +23,9 @@
</concept>
<concept id="1071666914219" name="jetbrains.mps.lang.editor.structure.ConceptEditorDeclaration" flags="ig" index="24kQdi" />
<concept id="1597643335227097138" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_TransformationMenu_node" flags="ng" index="7Obwk" />
<concept id="6822301196700715228" name="jetbrains.mps.lang.editor.structure.ConceptEditorHintDeclarationReference" flags="ig" index="2aJ2om">
<reference id="5944657839026714445" name="hint" index="2$4xQ3" />
</concept>
<concept id="1140524381322" name="jetbrains.mps.lang.editor.structure.CellModel_ListWithRole" flags="ng" index="2czfm3">
<property id="1140524450557" name="separatorText" index="2czwfO" />
<child id="1140524464360" name="cellLayout" index="2czzBx" />
@ -29,8 +35,11 @@
<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="1106270549637" name="jetbrains.mps.lang.editor.structure.CellLayout_Horizontal" flags="nn" index="2iRfu4" />
<concept id="1106270571710" name="jetbrains.mps.lang.editor.structure.CellLayout_Vertical" flags="nn" index="2iRkQZ" />
<concept id="3459162043708467089" name="jetbrains.mps.lang.editor.structure.CellActionMap_CanExecuteFunction" flags="in" index="jK8Ss" />
<concept id="1237303669825" name="jetbrains.mps.lang.editor.structure.CellLayout_Indent" flags="nn" index="l2Vlx" />
<concept id="1237308012275" name="jetbrains.mps.lang.editor.structure.IndentLayoutNewLineStyleClassItem" flags="ln" index="ljvvj" />
<concept id="1233148810477" name="jetbrains.mps.lang.editor.structure.InlineStyleDeclaration" flags="ng" index="tppnM" />
<concept id="1177327274449" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_pattern" flags="nn" index="ub8z3" />
<concept id="1177327570013" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_Substitute" flags="in" index="ucgPf" />
@ -38,6 +47,9 @@
<child id="8478191136883534238" name="features" index="upBLP" />
</concept>
<concept id="1177335944525" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_SubstituteString" flags="in" index="uGdhv" />
<concept id="4242538589859161874" name="jetbrains.mps.lang.editor.structure.ExplicitHintsSpecification" flags="ng" index="2w$q5c">
<child id="4242538589859162459" name="hints" index="2w$qW5" />
</concept>
<concept id="1080736578640" name="jetbrains.mps.lang.editor.structure.BaseEditorComponent" flags="ig" index="2wURMF">
<child id="1080736633877" name="cellModel" index="2wV5jI" />
</concept>
@ -51,6 +63,9 @@
<child id="1638911550608610281" name="executeFunction" index="IWgqQ" />
<child id="5692353713941573325" name="textFunction" index="1hCUd6" />
</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="4323500428121233431" name="jetbrains.mps.lang.editor.structure.EditorCellId" flags="ng" index="2SqB2G" />
<concept id="4323500428136740385" name="jetbrains.mps.lang.editor.structure.CellIdReferenceSelector" flags="ng" index="2TlHUq">
<reference id="4323500428136742952" name="id" index="2TlMyj" />
@ -59,6 +74,7 @@
<property id="1186414551515" name="flag" index="VOm3f" />
</concept>
<concept id="1186414860679" name="jetbrains.mps.lang.editor.structure.EditableStyleClassItem" flags="ln" index="VPxyj" />
<concept id="1186414928363" name="jetbrains.mps.lang.editor.structure.SelectableStyleSheetItem" flags="ln" index="VPM3Z" />
<concept id="1630016958697718209" name="jetbrains.mps.lang.editor.structure.IMenuReference_Default" flags="ng" index="2Z_bC8">
<reference id="1630016958698373342" name="concept" index="2ZyFGn" />
</concept>
@ -93,6 +109,7 @@
<concept id="5692353713941573329" name="jetbrains.mps.lang.editor.structure.QueryFunction_TransformationMenu_ActionLabelText" flags="ig" index="1hCUdq" />
<concept id="3308396621974580100" name="jetbrains.mps.lang.editor.structure.SubstituteMenu_Default" flags="ng" index="3p36aQ" />
<concept id="1139848536355" name="jetbrains.mps.lang.editor.structure.CellModel_WithRole" flags="ng" index="1$h60E">
<property id="1139852716018" name="noTargetText" index="1$x2rV" />
<reference id="1140103550593" name="relationDeclaration" index="1NtTu8" />
</concept>
<concept id="1073389214265" name="jetbrains.mps.lang.editor.structure.EditorCellModel" flags="ng" index="3EYTF0">
@ -113,7 +130,9 @@
<child id="1219418656006" name="styleItem" index="3F10Kt" />
</concept>
<concept id="1073389882823" name="jetbrains.mps.lang.editor.structure.CellModel_RefNode" flags="sg" stub="730538219795960754" index="3F1sOY" />
<concept id="1073390211982" name="jetbrains.mps.lang.editor.structure.CellModel_RefNodeList" flags="sg" stub="2794558372793454595" index="3F2HdR" />
<concept id="1073390211982" name="jetbrains.mps.lang.editor.structure.CellModel_RefNodeList" flags="sg" stub="2794558372793454595" index="3F2HdR">
<child id="7279578193766667846" name="addHints" index="78xua" />
</concept>
<concept id="5624877018228267058" name="jetbrains.mps.lang.editor.structure.ITransformationMenu" flags="ng" index="3INCJE">
<child id="1638911550608572412" name="sections" index="IW6Ez" />
</concept>
@ -202,6 +221,9 @@
</concept>
</language>
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
<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>
@ -230,6 +252,7 @@
</language>
</registry>
<node concept="24kQdi" id="2DPo4JTS3fE">
<property role="3GE5qa" value="sentence" />
<ref role="1XX52x" to="bw37:2DPo4JTRwsP" resolve="Function" />
<node concept="3EZMnI" id="2DPo4JTS3fG" role="2wV5jI">
<node concept="3F0A7n" id="2DPo4JTS3fN" role="3EZMnx">
@ -274,6 +297,7 @@
</node>
</node>
<node concept="24kQdi" id="2DPo4JTS3gx">
<property role="3GE5qa" value="sentence" />
<ref role="1XX52x" to="bw37:2DPo4JTRwsM" resolve="Variable" />
<node concept="3EZMnI" id="2DPo4JTS3gz" role="2wV5jI">
<node concept="3F0A7n" id="2DPo4JTS3gE" role="3EZMnx">
@ -283,6 +307,7 @@
</node>
</node>
<node concept="24kQdi" id="2DPo4JTS3gH">
<property role="3GE5qa" value="sentence" />
<ref role="1XX52x" to="bw37:2DPo4JTRwsI" resolve="Object" />
<node concept="3EZMnI" id="2DPo4JTS3gJ" role="2wV5jI">
<node concept="3F0A7n" id="2DPo4JTS3gQ" role="3EZMnx">
@ -292,6 +317,7 @@
</node>
</node>
<node concept="24kQdi" id="2DPo4JTS3gT">
<property role="3GE5qa" value="sentence" />
<ref role="1XX52x" to="bw37:2DPo4JTRwtx" resolve="Relation" />
<node concept="3EZMnI" id="2DPo4JTS3gV" role="2wV5jI">
<node concept="3F0A7n" id="2DPo4JTS3gW" role="3EZMnx">
@ -339,6 +365,7 @@
</node>
</node>
<node concept="24kQdi" id="2DPo4JTS3hE">
<property role="3GE5qa" value="sentence" />
<ref role="1XX52x" to="bw37:2DPo4JTRwtd" resolve="Forall" />
<node concept="3EZMnI" id="2DPo4JTSb6B" role="2wV5jI">
<node concept="3F0ifn" id="2DPo4JTSb6C" role="3EZMnx">
@ -363,6 +390,7 @@
</node>
</node>
<node concept="24kQdi" id="2DPo4JTS3hT">
<property role="3GE5qa" value="sentence" />
<ref role="1XX52x" to="bw37:2DPo4JTRwtj" resolve="Exists" />
<node concept="3EZMnI" id="2DPo4JTS3hV" role="2wV5jI">
<node concept="3F0ifn" id="2DPo4JTS3i2" role="3EZMnx">
@ -473,6 +501,7 @@
</node>
</node>
<node concept="IW6AY" id="2DPo4JTT2gW">
<property role="3GE5qa" value="sentence" />
<ref role="aqKnT" to="bw37:2DPo4JTRwsI" resolve="Object" />
<node concept="1Qtc8_" id="2DPo4JTT2gX" role="IW6Ez">
<node concept="IWgqT" id="2DPo4JTT2gY" role="1Qtc8A">
@ -557,6 +586,7 @@
</node>
<node concept="1h_SRR" id="2DPo4JTT9wr">
<property role="TrG5h" value="Function_DeleteArguments" />
<property role="3GE5qa" value="sentence" />
<ref role="1h_SK9" to="bw37:2DPo4JTRwsP" resolve="Function" />
<node concept="1hA7zw" id="2DPo4JTT9BG" role="1h_SK8">
<property role="1hAc7j" value="delete_action_id" />
@ -629,6 +659,7 @@
</node>
<node concept="1h_SRR" id="2DPo4JTTm8h">
<property role="TrG5h" value="Relation_DeleteMembers" />
<property role="3GE5qa" value="sentence" />
<ref role="1h_SK9" to="bw37:2DPo4JTRwtx" resolve="Relation" />
<node concept="1hA7zw" id="2DPo4JTTm8i" role="1h_SK8">
<property role="1hAc7j" value="delete_action_id" />
@ -700,6 +731,7 @@
</node>
</node>
<node concept="3p36aQ" id="2DPo4JTTz2r">
<property role="3GE5qa" value="sentence" />
<ref role="aqKnT" to="bw37:2DPo4JTRwsI" resolve="Object" />
<node concept="3eGOop" id="2DPo4JTTz6H" role="3ft7WO">
<node concept="16NL0t" id="2DPo4JTTA7L" role="upBLP">
@ -751,6 +783,7 @@
</node>
</node>
<node concept="3p36aQ" id="2DPo4JTTRkl">
<property role="3GE5qa" value="sentence" />
<ref role="aqKnT" to="bw37:2DPo4JTRwsM" resolve="Variable" />
<node concept="3eGOop" id="2DPo4JTTRkm" role="3ft7WO">
<node concept="16NL0t" id="2DPo4JTTRkn" role="upBLP">
@ -802,10 +835,161 @@
</node>
</node>
<node concept="3p36aQ" id="Vo$tzLCAJL">
<property role="3GE5qa" value="sentence" />
<ref role="aqKnT" to="bw37:2DPo4JTRwtx" resolve="Relation" />
</node>
<node concept="3p36aQ" id="Vo$tzLDB3M">
<property role="3GE5qa" value="sentence" />
<ref role="aqKnT" to="bw37:2DPo4JTRwsP" resolve="Function" />
</node>
<node concept="24kQdi" id="3w0n0hzhND_">
<property role="3GE5qa" value="proof" />
<ref role="1XX52x" to="bw37:3w0n0hzg5do" resolve="HerbrandProof" />
<node concept="3EZMnI" id="3JXBM6C3URi" role="2wV5jI">
<node concept="PMmxH" id="3w0n0hzhNuL" role="3EZMnx">
<ref role="PMmxG" to="tpco:2wZex4PafBj" resolve="alias" />
</node>
<node concept="3F0A7n" id="3JXBM6C4h$I" role="3EZMnx">
<ref role="1NtTu8" to="tpck:h0TrG11" resolve="name" />
<node concept="ljvvj" id="3JXBM6C4h$R" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="3F0ifn" id="2AfSc6Jvjpp" role="3EZMnx">
<property role="3F0ifm" value="" />
<node concept="ljvvj" id="2AfSc6Jvjpq" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="3F0A7n" id="2AfSc6Jvjoy" role="3EZMnx">
<ref role="1NtTu8" to="jfgh:2AfSc6Jvjow" resolve="description" />
<node concept="ljvvj" id="2AfSc6Jvjs0" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="3F0ifn" id="$u9BK__SIy" role="3EZMnx">
<property role="3F0ifm" value="" />
<node concept="ljvvj" id="$u9BK__SJr" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="3EZMnI" id="$u9BK__SDZ" role="3EZMnx">
<node concept="ljvvj" id="$u9BK__SHA" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
<node concept="VPM3Z" id="$u9BK__SE1" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="3F0ifn" id="$u9BK__SFC" role="3EZMnx">
<property role="3F0ifm" value="Goal:" />
</node>
<node concept="l2Vlx" id="$u9BK__SE4" role="2iSdaV" />
<node concept="3F1sOY" id="$u9BK__SCz" role="3EZMnx">
<property role="1$x2rV" value="&lt;no goal&gt;" />
<ref role="1NtTu8" to="jfgh:$u9BK__SAr" resolve="goal" />
</node>
</node>
<node concept="3EZMnI" id="$u9BK__SGu" role="3EZMnx">
<node concept="VPM3Z" id="$u9BK__SGw" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="ljvvj" id="$u9BK__SHv" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
<node concept="3F0ifn" id="$u9BK__SHp" role="3EZMnx">
<property role="3F0ifm" value="Proof:" />
</node>
<node concept="l2Vlx" id="$u9BK__SGz" role="2iSdaV" />
</node>
<node concept="3EZMnI" id="$u9BK_yCN6" role="3EZMnx">
<node concept="3EZMnI" id="$u9BK_z1QP" role="3EZMnx">
<node concept="VPM3Z" id="$u9BK_z1QR" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="2iRkQZ" id="$u9BK_z1QU" role="2iSdaV" />
<node concept="3EZMnI" id="$u9BK_z6et" role="3EZMnx">
<node concept="l2Vlx" id="$u9BK_z6eu" role="2iSdaV" />
<node concept="VPM3Z" id="$u9BK_z6ev" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="3F2HdR" id="$u9BK_z6ez" role="3EZMnx">
<property role="2czwfO" value=" " />
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
<node concept="l2Vlx" id="$u9BK_z6e$" role="2czzBx" />
<node concept="tppnM" id="$u9BK_zt0T" role="sWeuL">
<node concept="ljvvj" id="$u9BK_zt0V" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="2w$q5c" id="5RfK0kxj3Yz" role="78xua">
<node concept="2aJ2om" id="5RfK0kxj3Y$" role="2w$qW5">
<ref role="2$4xQ3" to="8v9h:$u9BK_z27v" resolve="ID" />
</node>
</node>
</node>
</node>
</node>
<node concept="3EZMnI" id="$u9BK_yCN7" role="3EZMnx">
<node concept="VPM3Z" id="$u9BK_yCN8" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="2iRkQZ" id="$u9BK_yCNa" role="2iSdaV" />
<node concept="3EZMnI" id="3JXBM6C6j0E" role="3EZMnx">
<node concept="VPM3Z" id="3JXBM6C6j0G" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="l2Vlx" id="3JXBM6C6j0J" role="2iSdaV" />
<node concept="3F2HdR" id="3JXBM6C3URp" role="3EZMnx">
<property role="2czwfO" value=" " />
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
<node concept="l2Vlx" id="3JXBM6C3URr" role="2czzBx" />
<node concept="tppnM" id="3JXBM6C3URw" role="sWeuL">
<node concept="ljvvj" id="3JXBM6C3URy" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="3F0ifn" id="3JXBM6C3UR$" role="2czzBI">
<property role="3F0ifm" value="" />
<property role="ilYzB" value="&lt;no steps&gt;" />
</node>
</node>
</node>
</node>
<node concept="2iRfu4" id="$u9BK_yCNb" role="2iSdaV" />
<node concept="3EZMnI" id="$u9BK_zG5o" role="3EZMnx">
<node concept="3EZMnI" id="$u9BK_$Qxk" role="3EZMnx">
<node concept="l2Vlx" id="$u9BK_$Qxl" role="2iSdaV" />
<node concept="VPM3Z" id="$u9BK_$Qxm" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="3F2HdR" id="$u9BK_$Qxn" role="3EZMnx">
<property role="2czwfO" value=" " />
<ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
<node concept="l2Vlx" id="$u9BK_$Qxo" role="2czzBx" />
<node concept="tppnM" id="$u9BK_$Qxp" role="sWeuL">
<node concept="ljvvj" id="$u9BK_$Qxq" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="2w$q5c" id="$u9BK_$QxA" role="78xua">
<node concept="2aJ2om" id="$u9BK_$QxB" role="2w$qW5">
<ref role="2$4xQ3" to="8v9h:$u9BK_zG6f" resolve="BASIS" />
</node>
</node>
</node>
</node>
<node concept="VPM3Z" id="$u9BK_zG5q" role="3F10Kt">
<property role="VOm3f" value="false" />
</node>
<node concept="2iRkQZ" id="$u9BK_zG5t" role="2iSdaV" />
</node>
</node>
<node concept="l2Vlx" id="3JXBM6C3URl" role="2iSdaV" />
</node>
</node>
<node concept="3p36aQ" id="3w0n0hzhNHg">
<property role="3GE5qa" value="proof" />
<ref role="aqKnT" to="bw37:3w0n0hzg5do" resolve="HerbrandProof" />
</node>
</model>

74
samples/fitch/languages/jetbrains.mps.logic.herbrand/models/structure.mps
View File

@ -23,6 +23,7 @@
<reference id="1169127628841" name="intfc" index="PrY4T" />
</concept>
<concept id="1071489090640" name="jetbrains.mps.lang.structure.structure.ConceptDeclaration" flags="ig" index="1TIwiD">
<property id="1096454100552" name="rootable" index="19KtqR" />
<reference id="1071489389519" name="extends" index="1TJDcQ" />
<child id="1169129564478" name="implements" index="PzmwI" />
</concept>
@ -35,6 +36,9 @@
</concept>
</language>
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
<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>
@ -44,6 +48,7 @@
<property role="EcuMT" value="3059457401299011374" />
<property role="TrG5h" value="Object" />
<property role="34LRSv" value="object" />
<property role="3GE5qa" value="sentence" />
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
<node concept="PrWs8" id="2DPo4JTRwt9" role="PzmwI">
<ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
@ -55,11 +60,13 @@
<node concept="PlHQZ" id="2DPo4JTRwsJ">
<property role="EcuMT" value="3059457401299011375" />
<property role="TrG5h" value="Term" />
<property role="3GE5qa" value="sentence" />
</node>
<node concept="1TIwiD" id="2DPo4JTRwsM">
<property role="EcuMT" value="3059457401299011378" />
<property role="TrG5h" value="Variable" />
<property role="34LRSv" value="variable" />
<property role="3GE5qa" value="sentence" />
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
<node concept="PrWs8" id="2DPo4JTRwt2" role="PzmwI">
<ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
@ -72,6 +79,7 @@
<property role="EcuMT" value="3059457401299011381" />
<property role="TrG5h" value="Function" />
<property role="34LRSv" value="function" />
<property role="3GE5qa" value="sentence" />
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
<node concept="1TJgyj" id="2DPo4JTRwtv" role="1TKVEi">
<property role="IQ2ns" value="3059457401299011423" />
@ -92,6 +100,7 @@
<property role="TrG5h" value="Forall" />
<property role="34LRSv" value="forall" />
<property role="R4oN_" value="Universal Sentence" />
<property role="3GE5qa" value="sentence" />
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
<node concept="1TJgyj" id="2DPo4JTRwtr" role="1TKVEi">
<property role="IQ2ns" value="3059457401299011419" />
@ -116,6 +125,7 @@
<property role="TrG5h" value="Exists" />
<property role="34LRSv" value="exists" />
<property role="R4oN_" value="Existentional Sentence" />
<property role="3GE5qa" value="sentence" />
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
<node concept="1TJgyj" id="2DPo4JTRwto" role="1TKVEi">
<property role="IQ2ns" value="3059457401299011416" />
@ -140,6 +150,7 @@
<property role="TrG5h" value="Relation" />
<property role="34LRSv" value="relation" />
<property role="R4oN_" value="Relational" />
<property role="3GE5qa" value="sentence" />
<ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
<node concept="1TJgyj" id="2DPo4JTRwtF" role="1TKVEi">
<property role="IQ2ns" value="3059457401299011435" />
@ -155,5 +166,68 @@
<ref role="PrY4T" to="jfgh:4LBPYGV4cY1" resolve="Sentence" />
</node>
</node>
<node concept="1TIwiD" id="Vo$tzLEGtD">
<property role="EcuMT" value="1069765272453957481" />
<property role="TrG5h" value="ForallIntro" />
<property role="34LRSv" value="∀I" />
<property role="R4oN_" value="Universal Introduction" />
<property role="3GE5qa" value="proof.rule" />
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
<node concept="PrWs8" id="3w0n0hzjEBR" role="PzmwI">
<ref role="PrY4T" node="3w0n0hziLce" resolve="QuantifierRule" />
</node>
</node>
<node concept="1TIwiD" id="Vo$tzLEGtE">
<property role="EcuMT" value="1069765272453957482" />
<property role="TrG5h" value="ForallElim" />
<property role="34LRSv" value="∀E" />
<property role="R4oN_" value="Universal Elimination" />
<property role="3GE5qa" value="proof.rule" />
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
<node concept="PrWs8" id="3w0n0hzjEBP" role="PzmwI">
<ref role="PrY4T" node="3w0n0hziLce" resolve="QuantifierRule" />
</node>
</node>
<node concept="1TIwiD" id="Vo$tzLEGtF">
<property role="EcuMT" value="1069765272453957483" />
<property role="TrG5h" value="ExistsIntro" />
<property role="34LRSv" value="∃I" />
<property role="R4oN_" value="Existential Introduction" />
<property role="3GE5qa" value="proof.rule" />
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
<node concept="PrWs8" id="3w0n0hzjEBN" role="PzmwI">
<ref role="PrY4T" node="3w0n0hziLce" resolve="QuantifierRule" />
</node>
</node>
<node concept="1TIwiD" id="Vo$tzLEGtG">
<property role="EcuMT" value="1069765272453957484" />
<property role="TrG5h" value="ExistsElim" />
<property role="34LRSv" value="∃E" />
<property role="R4oN_" value="Existential Elimination" />
<property role="3GE5qa" value="proof.rule" />
<ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
<node concept="PrWs8" id="3w0n0hzjEBL" role="PzmwI">
<ref role="PrY4T" node="3w0n0hziLce" resolve="QuantifierRule" />
</node>
</node>
<node concept="1TIwiD" id="3w0n0hzg5do">
<property role="EcuMT" value="4035326440038749016" />
<property role="TrG5h" value="HerbrandProof" />
<property role="19KtqR" value="true" />
<property role="34LRSv" value="Herbrand Proof" />
<property role="3GE5qa" value="proof" />
<ref role="1TJDcQ" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
<node concept="PrWs8" id="3w0n0hzg5dp" role="PzmwI">
<ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
</node>
<node concept="PrWs8" id="3w0n0hzg5du" role="PzmwI">
<ref role="PrY4T" to="jfgh:3JXBM6C5urr" resolve="Root" />
</node>
</node>
<node concept="PlHQZ" id="3w0n0hziLce">
<property role="EcuMT" value="4035326440039453454" />
<property role="3GE5qa" value="proof.rule" />
<property role="TrG5h" value="QuantifierRule" />
</node>
</model>

3542
samples/fitch/languages/jetbrains.mps.logic.herbrand/models/types.mps Normal file
View File

File diff suppressed because it is too large Load Diff