I'm not sure whether this is a better fit for TeX.SE or Stackoverflow, but given that it's mostly TeX-centric, I figured the TeX hive mind here would be the best fit.

I'd like to have a GUI document processor for writing fitch-style logic proofs, like those created with the LPLFitch package. I'd want it to be entirely WYSIWYG (what you see is what you get), without requiring the user to interact with the TeX code directly, but using LaTeX in the back-end. Additionally, I'd like to have it be entirely self-contained, not requiring an installation of LaTeX on the user's machine. It would be used to help students with not TeX experience produce such proofs.

The question I have is what existing, open source, resources are there out there? The only thing of the sort I'm familiar with is LyX, but that aims at a full scale implementation of LaTeX, as opposed to the very minimal processor I have in mind, which would utilize only a very small number of packages and minimal subset of LaTeX's full power.

The goal:

  1. Document processor that is entirely WYSIWYG.
  2. Would have a few buttons to insert the necessary symbols, and would render those symbols immediately (either by inserting them as unicode symbols, or a quick compilation run).
  3. Wouldn't require knowledge of LaTeX on the user-end, and wouldn't require a full LaTeX installation on users' machines.
  4. Would produce Fitch-style natural deduction proofs, like those in the LPLFitch package.

The questions:

  1. What existing open source resources are out there that I could build off of?
  2. What advice would you have for implementing something like this from scratch (e.g., use LuaTeX or some more programmatic flavor of TeX)?
  3. Is this even a good idea, or am I just letting my familiarity with LaTeX blind me to better solutions?

I realize this is a pretty open-ended and underdeveloped question. It's an idea I'm just starting out with and something I don't have a slew of experience with, but a project I'd like to pursue. I understand fully if the question is not appropriate for the site in its current form.

  • Given your goal, how wedded are you to the idea of using TeX on the backend? (LaTeX is a document preparation language that is aimed at authors; if your authors will not see LaTeX, why use LaTeX?) // On the flipped side, if you want to use LaTeX, then training students to use (some subset) of the TeX markup is not too difficult. (The intro to proofs class I taught two years ago successfully got close to 200 students writing not-entirely-abominable TeX incantations within two weeks of start of class.) If you don't want to worry about software, use something like SageMathCloud or ShareLatex Jun 30 '17 at 19:33
  • @WillieWong I'd be willing to abandon TeX on the backend if that just turns out to be too much trouble to be worth the effort. The main reason I'd like to use it is just that I already have fairly robust templates for formatting the proofs in the style of the book I use. But perhaps the best route is to just abandon TeX.
    – Dennis
    Jun 30 '17 at 19:36
  • 1
    Google brought me to FitchJS which has a live version here. It claims to export in TeX. I am not familiar with Fitch-style proofs to type anything useful in the live version to test it. You should give it a try. Jun 30 '17 at 19:46
  • 1
    Proofmood apparently also has a couple of Fitch-style proof builders, and they also have "TeX export" buttons on their interfaces. Jun 30 '17 at 19:47
  • @WillieWong Wow! My Google-fu is weak, apparently! I'm on mobile right now, but will test them in a few minute when I'm back at a computer. Im optimistic that at least one of them will do the trick. I'm encouraging ShareLaTeX use, and have provided detailed templates that simplify a lot. But since it's an accelerated summer course their first test is a week after the course begins. Add to that the fact that most of my students will be humanities students with little to no CS or post high school math, and I'm a bit pessimistic that they'll pick up LaTeX that quickly.
    – Dennis
    Jun 30 '17 at 19:57

Two web-based services do something approximately similar to what is asked in the question. In both cases the service support some sort of TeX export; however neither use the lplfitch package referenced in the original question.

  • FitchJS (see also live version) exports into a format using Johan Klüwer's fitch.sty package. (A copy is available on LogicMatters as well as in the Git repo for the fitchjs project.)
  • Proofmood outputs in their own custom format; but it is not clear if their code is open-source. (The development also seems more active for the Korean version compared to the English version.)

It quite possible to fork FitchJS and get it to use lplfitch: the code for handling the LaTeX generation are in two files:

  1. In parsing.js there is a part where unicode symbols gets translated to and from their LaTeX equivalents. lplfitch uses different micros for the connectives; this part should be an easy fix.

  2. Slightly more complicated is the export routine in userio.js; the syntax for the fitch package is substantially different from the syntax for adding a proof line in the lplfitch package, and will require a bit more time investment to re-write.

    (It appears that the proof is stored on a stack internally (if my cursory look is correct), in which case it may be better to dump the existing export routine and write something new, which is based on converting the proofs first to lines and then converting individual lines (including the correct number of vertical bars) into one line in the output, entirely ignoring the logical structure. This is the entire opposite of what lplfitch wants.)

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.