Procesador WYSIWYG mínimo para pruebas estilo Fitch con backend LaTeX

Question

No estoy seguro de si esto encaja mejor con TeX.SE o Stackoverflow, pero dado que está principalmente centrado en TeX, pensé que la mente de colmena TeX aquí sería la mejor opción.

Me gustaría tener un procesador de documentos GUI para escribir pruebas lógicas estilo Fitch, como las creadas con elPaquete LPLFitch. Me gustaría que fuera completamente WYSIWYG (lo que ves es lo que obtienes), sin requerir que el usuario interactúe con el código TeX directamente, sino usando LaTeX en el back-end. Además, me gustaría que fuera completamente autónomo y que no requiriera la instalación de LaTeX en la máquina del usuario. Se utilizaría para ayudar a los estudiantes sin experiencia en TeX a producir tales pruebas.

La pregunta que tengo es ¿qué recursos existentes de código abierto existen? Lo único que conozco esLyX, pero eso apunta a una implementación a gran escala de LaTeX, a diferencia del procesador mínimo que tengo en mente, que utilizaría solo una cantidad muy pequeña de paquetes y un subconjunto mínimo de la potencia total de LaTeX.

La meta:

1. Procesador de documentos completamente WYSIWYG.
2. Tendría algunos botones para insertar los símbolos necesarios y los representaría inmediatamente (ya sea insertándolos como símbolos Unicode o mediante una ejecución de compilación rápida).
3. No requeriría conocimientos de LaTeX por parte del usuario y no requeriría una instalación completa de LaTeX en las máquinas de los usuarios.
4. Produciría pruebas de deducción natural al estilo de Fitch, como las del paquete LPLFitch.

Las preguntas:

1. ¿Qué recursos de código abierto existentes existen a partir de los cuales podría aprovechar?
2. ¿Qué consejo daría para implementar algo como esto desde cero (por ejemplo, usar LuaTeX o alguna versión más programática de TeX)?
3. ¿Es esto siquiera una buena idea, o simplemente estoy dejando que mi familiaridad con LaTeX me ciegue a mejores soluciones?

Me doy cuenta de que esta es una pregunta bastante abierta y poco desarrollada. Es una idea con la que recién estoy comenzando y algo en lo que no tengo mucha experiencia, pero es un proyecto que me gustaría seguir. Entiendo completamente si la pregunta no es apropiada para el sitio en su forma actual.

Answer 1

Dos servicios basados ​​en web hacen algo aproximadamente similar a lo que se pregunta en la pregunta. En ambos casos, el servicio admite algún tipo de exportación TeX; sin embargo, ninguno de los dos utilice el lplfitchpaquete al que se hace referencia en la pregunta original.

• FitchJS(ver tambiénversión en vivo) exporta a un formato que utiliza el paquete de Johan Klüwer fitch.sty. (Hay una copia disponible enLa lógica importaasí como en el repositorio de Git del fitchjsproyecto).
• estado de ánimo a pruebasalidas en su propioformato personalizado; pero no está claro si su código es de código abierto. (El desarrollo también parece más activo para la versión coreana en comparación con la versión en inglés).

Es muy posible bifurcarlo FitchJSy usarlo lplfitch: el código para manejar la generación LaTeX está en dos archivos:

1. Hay parsing.jsuna parte donde los símbolos Unicode se traducen hacia y desde sus equivalentes LaTeX. lplfitchutiliza diferentes micros para los conectivos; Esta parte debería tener una solución fácil.

2. Un poco más complicada es la rutina de exportación en userio.js; la sintaxis del fitchpaquete es sustancialmente diferente de la sintaxis para agregar una línea de prueba en el lplfitchpaquete y requerirá un poco más de tiempo para reescribirla.

   (Parece que la prueba está almacenada en una pila internamente (si mi mirada superficial es correcta), en cuyo caso puede ser mejor deshacerse de la rutina de exportación existente y escribir algo nuevo, que se base en convertir las pruebas primero en líneas y luego convertir líneas individuales (incluido el número correcto de barras verticales) en una línea en la salida, ignorando por completo la estructura lógica. Esto es todo lo contrario de lo que lplfitchquiere).