KWARC / FoMID

0 stars 0 forks source link

Natural language annotations in general #1

Open Jazzpirate opened 3 years ago

Jazzpirate commented 3 years ago

Example sentence

"A natural number $N$ is even, if its square is even."

Requirements

Ideas

=> \implication*[2]{\even{A \NaturalNumbers[natural number] $N$}[ is even]}[, if]{\even{\natpow{its}*{2}[ square]}[ is even]}.

Remaining questions

  1. Both "A natural number $N$" and "its" represent OMV(N), where N has type \NaturalNumbers and is universally quantified. How to represent this? (see https://github.com/KWARC/FoMID/issues/5 )
  2. Binding applications (see https://github.com/KWARC/FoMID/issues/8 )
  3. Sequences (see https://github.com/KWARC/FoMID/issues/7 )
Jazzpirate commented 3 years ago

Update: Things get tricky with associative arguments.

Possible solution 1: \operator just takes arbitrarily many arguments in general (via \ifnextchar[ and \ifnextchar{ - need to check whether the latter works even). Inelegant, but would probably work.

Possible solution 2: an associative argument takes arbitrarily many comma-separated arguments, every other of which is considered a verbalization component. E.g. for flexary \plus, an application could look something like \plus[the sum of ]{a,{,},b, and ,c}