Minimaler WYSIWYG-Prozessor für Beweise im Fitch-Stil mit LaTeX-Backend

Question

Ich bin nicht sicher, ob dies besser zu TeX.SE oder Stackoverflow passt, aber da es hauptsächlich TeX-zentriert ist, dachte ich, dass das TeX-Hive-Mind hier am besten passen würde.

Ich hätte gerne einen GUI-Dokumentprozessor zum Schreiben logischer Beweise im Fitch-Stil, wie sie mit demLPLFitch-Paket. Ich möchte, dass es vollständig WYSIWYG (What You See Is What You Get) ist, ohne dass der Benutzer direkt mit dem TeX-Code interagieren muss, sondern LaTeX im Backend verwendet. Darüber hinaus möchte ich, dass es vollständig in sich geschlossen ist und keine Installation von LaTeX auf dem Computer des Benutzers erfordert. Es würde verwendet werden, um Studenten ohne TeX-Erfahrung bei der Erstellung solcher Beweise zu helfen.

Die Frage, die ich habe, ist, welche bestehenden Open-Source-Ressourcen es gibt. Das einzige, was ich kenne, istLyX, das aber auf eine vollständige Implementierung von LaTeX abzielt, im Gegensatz zu dem sehr minimalen Prozessor, den ich im Sinn habe, der nur eine sehr kleine Anzahl von Paketen und einen minimalen Teil der gesamten Leistung von LaTeX nutzen würde.

Das Ziel:

1. Vollständiger WYSIWYG-Dokumentenprozessor.
2. Hätte ein paar Schaltflächen zum Einfügen der erforderlichen Symbole und würde diese Symbole sofort rendern (entweder durch Einfügen als Unicode-Symbole oder durch einen schnellen Kompilierungslauf).
3. Auf Benutzerseite wären keine Kenntnisse von LaTeX erforderlich und auf den Computern der Benutzer wäre keine vollständige LaTeX-Installation erforderlich.
4. Würde Beweise für natürliche Deduktion im Fitch-Stil erzeugen, wie die im LPLFitch-Paket.

Die Fragen:

1. Welche vorhandenen Open-Source-Ressourcen gibt es, auf denen ich aufbauen könnte?
2. Welchen Rat würden Sie für die Implementierung so etwas von Grund auf geben (z. B. Verwendung von LuaTeX oder einer programmatischeren Variante von TeX)?
3. Ist das überhaupt eine gute Idee, oder lasse ich mich durch meine Vertrautheit mit LaTeX für bessere Lösungen blind machen?

Mir ist klar, dass dies eine ziemlich offene und unterentwickelte Frage ist. Es ist eine Idee, mit der ich gerade erst beginne und mit der ich nicht viel Erfahrung habe, aber es ist ein Projekt, das ich gerne verfolgen würde. Ich verstehe vollkommen, wenn die Frage in ihrer aktuellen Form nicht für die Site geeignet ist.

Answer 1

Zwei webbasierte Dienste tun ungefähr das Gleiche wie in der Frage beschrieben. In beiden Fällen unterstützt der Dienst eine Art TeX-Export. Allerdings verwendet keiner von beiden das lplfitchin der ursprünglichen Frage referenzierte Paket.

• FitchJS(siehe auchLive-Version) exportiert in ein Format, das Johan Klüwers fitch.styPaket verwendet. (Eine Kopie ist verfügbar aufLogik ist wichtigsowie im Git-Repo für das fitchjsProjekt.)
• BeweisstimmungAusgänge in ihren eigenenBenutzerdefiniertes Format; es ist jedoch nicht klar, ob ihr Code Open Source ist. (Außerdem scheint die Entwicklung der koreanischen Version im Vergleich zur englischen Version aktiver zu sein.)

Es ist durchaus möglich, es aufzuspalten FitchJSund nutzbar zu machen lplfitch: Der Code zur Handhabung der LaTeX-Generierung befindet sich in zwei Dateien:

1. Darin parsing.jsgibt es einen Teil, in dem Unicode-Symbole in ihre LaTeX-Äquivalente und umgekehrt übersetzt werden. lplfitchVerwendet unterschiedliche Mikros für die Konnektoren. Dieser Teil sollte leicht zu beheben sein.

2. Etwas komplizierter ist die Exportroutine in userio.js; die Syntax für das fitchPaket unterscheidet sich erheblich von der Syntax zum Hinzufügen einer Beweiszeile im lplfitchPaket und das Neuschreiben erfordert etwas mehr Zeitaufwand.

   (Es scheint, dass der Beweis intern auf einem Stapel gespeichert ist (wenn mein flüchtiger Blick richtig ist). In diesem Fall wäre es vielleicht besser, die vorhandene Exportroutine zu löschen und etwas Neues zu schreiben, das darauf basiert, die Beweise zuerst in Zeilen umzuwandeln und dann einzelne Zeilen (einschließlich der richtigen Anzahl vertikaler Striche) in der Ausgabe in eine Zeile umzuwandeln, wobei die logische Struktur völlig ignoriert wird. Dies ist das genaue Gegenteil von dem, was lplfitchwir wollen.)