Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Issue with 5 First-order_logic #26

Open
philsMINT opened this issue Jan 11, 2018 · 6 comments
Open

Issue with 5 First-order_logic #26

philsMINT opened this issue Jan 11, 2018 · 6 comments
Assignees
@philsMINT
Labels
major

Comments

@philsMINT
Copy link
Member

what about the scope of \forall quantors? position vertically instead of horizontally?
Link to First-order_logic, qID 5
@physikerwelt physikerwelt removed their assignment Jan 15, 2018
@gipplab gipplab deleted a comment from philsMINT Jan 18, 2018
@physikerwelt
Copy link
Member

There is http://www.w3.org/TR/MathML3/chapter4.html#contm.forall we should ensure that the generated MathML is according to this spec.

@physikerwelt physikerwelt assigned philsMINT and unassigned AndreG-P Jan 18, 2018
@physikerwelt
Copy link
Member

See also http://dlmf.nist.gov/LaTeXML/manual/customization/customization.latexml.html#SS1.SSS0.Px1 for details on the macro creation.

@philsMINT
Copy link
Member Author

philsMINT commented Jan 18, 2018 •
edited
Loading

tree looks good! macro \forallscope not used, delete?

@philsMINT philsMINT added question and removed major labels Jan 18, 2018
@physikerwelt physikerwelt removed their assignment Jan 18, 2018
@physikerwelt
Copy link
Member

@philsMINT the tree does not look good. There is no \times in the formulae.

@philsMINT
Copy link
Member Author

where do we need \times? the tree seems now to be branched logically correctly (even without using my macro \forallscope - should I delete it?)

@physikerwelt
Copy link
Member

@philsMINT I don't understand your question. The MathML, we currently visualize has times in it which is incorrect.

<math xmlns="http://www.w3.org/1998/Math/MathML"
      xmlns:xlink="http://www.w3.org/1999/xlink"
      alttext="\forall x\,\forall y\,P(x,y)\Leftrightarrow\forall y\,\forall x\,P(x,y)"
      class="ltx_Math"
      display="inline"
      id="p1.1.m1.1">
  <semantics id="p1.1.m1.1a">
      <mrow id="p1.1.m1.1.26" xref="p1.1.m1.1.26.cmml">
         <mrow id="p1.1.m1.1.26.1" xref="p1.1.m1.1.26.1.cmml">
            <mo id="p1.1.m1.1.1" xref="p1.1.m1.1.1.cmml">∀</mo>
            <mrow id="p1.1.m1.1.26.1.1" xref="p1.1.m1.1.26.1.1.cmml">
               <mpadded id="p1.1.m1.1.2" width="+1.7pt" xref="p1.1.m1.1.2.cmml">
                  <mi id="p1.1.m1.1.2a" xref="p1.1.m1.1.2.cmml">x</mi>
               </mpadded>
               <mo id="p1.1.m1.1.26.1.1.1" xref="p1.1.m1.1.26.1.1.1.cmml">⁢</mo>
               <mrow id="p1.1.m1.1.26.1.1.2" xref="p1.1.m1.1.26.1.1.2.cmml">
                  <mo id="p1.1.m1.1.4" xref="p1.1.m1.1.4.cmml">∀</mo>
                  <mrow id="p1.1.m1.1.26.1.1.2.1" xref="p1.1.m1.1.26.1.1.2.1.cmml">
                     <mpadded id="p1.1.m1.1.5" width="+1.7pt" xref="p1.1.m1.1.5.cmml">
                        <mi id="p1.1.m1.1.5a" xref="p1.1.m1.1.5.cmml">y</mi>
                     </mpadded>
                     <mo id="p1.1.m1.1.26.1.1.2.1.1" xref="p1.1.m1.1.26.1.1.2.1.1.cmml">⁢</mo>
                     <mrow id="p1.1.m1.1.26.1.1.2.1.2.2" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">
                        <mi id="p1.1.m1.1.7" xref="p1.1.m1.1.7.cmml">P</mi>
                        <mo id="p1.1.m1.1.26.1.1.2.1.2.2a" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">⁡</mo>
                        <mrow id="p1.1.m1.1.26.1.1.2.1.2.2.1" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">
                           <mo id="p1.1.m1.1.8"
                               stretchy="false"
                               xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">(</mo>
                           <mi id="p1.1.m1.1.9" xref="p1.1.m1.1.9.cmml">x</mi>
                           <mo id="p1.1.m1.1.10" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">,</mo>
                           <mi id="p1.1.m1.1.11" xref="p1.1.m1.1.11.cmml">y</mi>
                           <mo id="p1.1.m1.1.12"
                               stretchy="false"
                               xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">)</mo>
                        </mrow>
                     </mrow>
                  </mrow>
               </mrow>
            </mrow>
         </mrow>
         <mo id="p1.1.m1.1.13" xref="p1.1.m1.1.13.cmml">⇔</mo>
         <mrow id="p1.1.m1.1.26.2" xref="p1.1.m1.1.26.2.cmml">
            <mo id="p1.1.m1.1.14" xref="p1.1.m1.1.14.cmml">∀</mo>
            <mrow id="p1.1.m1.1.26.2.1" xref="p1.1.m1.1.26.2.1.cmml">
               <mpadded id="p1.1.m1.1.15" width="+1.7pt" xref="p1.1.m1.1.15.cmml">
                  <mi id="p1.1.m1.1.15a" xref="p1.1.m1.1.15.cmml">y</mi>
               </mpadded>
               <mo id="p1.1.m1.1.26.2.1.1" xref="p1.1.m1.1.26.2.1.1.cmml">⁢</mo>
               <mrow id="p1.1.m1.1.26.2.1.2" xref="p1.1.m1.1.26.2.1.2.cmml">
                  <mo id="p1.1.m1.1.17" xref="p1.1.m1.1.17.cmml">∀</mo>
                  <mrow id="p1.1.m1.1.26.2.1.2.1" xref="p1.1.m1.1.26.2.1.2.1.cmml">
                     <mpadded id="p1.1.m1.1.18" width="+1.7pt" xref="p1.1.m1.1.18.cmml">
                        <mi id="p1.1.m1.1.18a" xref="p1.1.m1.1.18.cmml">x</mi>
                     </mpadded>
                     <mo id="p1.1.m1.1.26.2.1.2.1.1" xref="p1.1.m1.1.26.2.1.2.1.1.cmml">⁢</mo>
                     <mrow id="p1.1.m1.1.26.2.1.2.1.2.2" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">
                        <mi id="p1.1.m1.1.20" xref="p1.1.m1.1.20.cmml">P</mi>
                        <mo id="p1.1.m1.1.26.2.1.2.1.2.2a" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">⁡</mo>
                        <mrow id="p1.1.m1.1.26.2.1.2.1.2.2.1" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">
                           <mo id="p1.1.m1.1.21"
                               stretchy="false"
                               xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">(</mo>
                           <mi id="p1.1.m1.1.22" xref="p1.1.m1.1.22.cmml">x</mi>
                           <mo id="p1.1.m1.1.23" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">,</mo>
                           <mi id="p1.1.m1.1.24" xref="p1.1.m1.1.24.cmml">y</mi>
                           <mo id="p1.1.m1.1.25"
                               stretchy="false"
                               xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">)</mo>
                        </mrow>
                     </mrow>
                  </mrow>
               </mrow>
            </mrow>
         </mrow>
      </mrow>
      <annotation-xml encoding="MathML-Content" id="p1.1.m1.1b">
         <apply id="p1.1.m1.1.26.cmml" xref="p1.1.m1.1.26">
            <ci id="p1.1.m1.1.13.cmml" xref="p1.1.m1.1.13">⇔</ci>
            <apply id="p1.1.m1.1.26.1.cmml" xref="p1.1.m1.1.26.1">
               <csymbol cd="latexml" id="p1.1.m1.1.1.cmml" xref="p1.1.m1.1.1">for-all</csymbol>
               <apply id="p1.1.m1.1.26.1.1.cmml" xref="p1.1.m1.1.26.1.1">
                  <times id="p1.1.m1.1.26.1.1.1.cmml" xref="p1.1.m1.1.26.1.1.1"/>
                  <ci id="p1.1.m1.1.2.cmml" xref="p1.1.m1.1.2">𝑥</ci>
                  <apply id="p1.1.m1.1.26.1.1.2.cmml" xref="p1.1.m1.1.26.1.1.2">
                     <csymbol cd="latexml" id="p1.1.m1.1.4.cmml" xref="p1.1.m1.1.4">for-all</csymbol>
                     <apply id="p1.1.m1.1.26.1.1.2.1.cmml" xref="p1.1.m1.1.26.1.1.2.1">
                        <times id="p1.1.m1.1.26.1.1.2.1.1.cmml" xref="p1.1.m1.1.26.1.1.2.1.1"/>
                        <ci id="p1.1.m1.1.5.cmml" xref="p1.1.m1.1.5">𝑦</ci>
                        <apply id="p1.1.m1.1.26.1.1.2.1.2.1.cmml" xref="p1.1.m1.1.26.1.1.2.1.2.2">
                           <csymbol cd="wikidata" id="p1.1.m1.1.7.cmml" xref="p1.1.m1.1.7">Q1144319</csymbol>
                           <ci id="p1.1.m1.1.9.cmml" xref="p1.1.m1.1.9">𝑥</ci>
                           <ci id="p1.1.m1.1.11.cmml" xref="p1.1.m1.1.11">𝑦</ci>
                        </apply>
                     </apply>
                  </apply>
               </apply>
            </apply>
            <apply id="p1.1.m1.1.26.2.cmml" xref="p1.1.m1.1.26.2">
               <csymbol cd="latexml" id="p1.1.m1.1.14.cmml" xref="p1.1.m1.1.14">for-all</csymbol>
               <apply id="p1.1.m1.1.26.2.1.cmml" xref="p1.1.m1.1.26.2.1">
                  <times id="p1.1.m1.1.26.2.1.1.cmml" xref="p1.1.m1.1.26.2.1.1"/>
                  <ci id="p1.1.m1.1.15.cmml" xref="p1.1.m1.1.15">𝑦</ci>
                  <apply id="p1.1.m1.1.26.2.1.2.cmml" xref="p1.1.m1.1.26.2.1.2">
                     <csymbol cd="latexml" id="p1.1.m1.1.17.cmml" xref="p1.1.m1.1.17">for-all</csymbol>
                     <apply id="p1.1.m1.1.26.2.1.2.1.cmml" xref="p1.1.m1.1.26.2.1.2.1">
                        <times id="p1.1.m1.1.26.2.1.2.1.1.cmml" xref="p1.1.m1.1.26.2.1.2.1.1"/>
                        <ci id="p1.1.m1.1.18.cmml" xref="p1.1.m1.1.18">𝑥</ci>
                        <apply id="p1.1.m1.1.26.2.1.2.1.2.1.cmml" xref="p1.1.m1.1.26.2.1.2.1.2.2">
                           <csymbol cd="wikidata" id="p1.1.m1.1.20.cmml" xref="p1.1.m1.1.20">Q1144319</csymbol>
                           <ci id="p1.1.m1.1.22.cmml" xref="p1.1.m1.1.22">𝑥</ci>
                           <ci id="p1.1.m1.1.24.cmml" xref="p1.1.m1.1.24">𝑦</ci>
                        </apply>
                     </apply>
                  </apply>
               </apply>
            </apply>
         </apply>
      </annotation-xml>
      <annotation encoding="application/x-tex" id="p1.1.m1.1c">\forall x\,\forall y\,P(x,y)\Leftrightarrow\forall y\,\forall x\,P(x,y)</annotation>
  </semantics>
</math>

@physikerwelt physikerwelt reopened this Jan 29, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@philsMINT philsMINT

Labels
major
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@physikerwelt @AndreG-P @philsMINT