Processador WYSIWYG mínimo para provas estilo Fitch com backend LaTeX

Question

Não tenho certeza se isso é mais adequado para TeX.SE ou Stackoverflow, mas como é principalmente centrado em TeX, imaginei que a mente coletiva do TeX aqui seria a melhor opção.

Eu gostaria de ter um processador de documentos GUI para escrever provas lógicas no estilo fitch, como aquelas criadas com oPacote LPLFitch. Eu gostaria que fosse totalmente WYSIWYG (o que você vê é o que você obtém), sem exigir que o usuário interaja diretamente com o código TeX, mas usando LaTeX no back-end. Além disso, gostaria que fosse totalmente independente, não exigindo instalação do LaTeX na máquina do usuário. Seria usado para ajudar alunos sem experiência em TeX a produzir tais provas.

A pergunta que tenho é quais recursos de código aberto existem por aí? A única coisa do tipo com a qual estou familiarizado éLyX, mas isso visa uma implementação em larga escala do LaTeX, em oposição ao processador mínimo que tenho em mente, que utilizaria apenas um número muito pequeno de pacotes e um subconjunto mínimo do poder total do LaTeX.

O objetivo:

1. Processador de documentos totalmente WYSIWYG.
2. Teria alguns botões para inserir os símbolos necessários e renderizaria esses símbolos imediatamente (inserindo-os como símbolos Unicode ou executando uma compilação rápida).
3. Não exigiria conhecimento de LaTeX por parte do usuário e não exigiria uma instalação completa do LaTeX nas máquinas dos usuários.
4. Produziria provas de dedução natural no estilo Fitch, como as do pacote LPLFitch.

As questões:

1. Quais recursos de código aberto existentes existem nos quais eu poderia desenvolver?
2. Que conselho você daria para implementar algo assim do zero (por exemplo, usar LuaTeX ou algum tipo mais programático de TeX)?
3. Isso é uma boa ideia ou estou apenas deixando minha familiaridade com o LaTeX me cegar para soluções melhores?

Sei que esta é uma questão bastante aberta e subdesenvolvida. É uma ideia que estou apenas começando e algo com o qual não tenho muita experiência, mas é um projeto que gostaria de prosseguir. Entendo perfeitamente se a pergunta não for apropriada para o site em sua forma atual.

Answer 1

Dois serviços baseados na web fazem algo aproximadamente semelhante ao que é perguntado na pergunta. Em ambos os casos, o serviço suporta algum tipo de exportação TeX; no entanto, nenhum dos dois usa o lplfitchpacote mencionado na pergunta original.

• Fitch JS(Veja tambémversão ao vivo) exporta para um formato que usa fitch.styo pacote de Johan Klüwer. (Uma cópia está disponível emLógica é importantebem como no repositório Git do fitchjsprojeto.)
• Prova de humorsaídas por conta própriaformato personalizado; mas não está claro se o código deles é de código aberto. (O desenvolvimento também parece mais ativo para a versão coreana em comparação com a versão inglesa.)

É bem possível fazer um fork FitchJSe usá-lo lplfitch: o código para lidar com a geração do LaTeX está em dois arquivos:

1. Há parsing.jsuma parte onde os símbolos Unicode são traduzidos de e para seus equivalentes em LaTeX. lplfitchutiliza diferentes micros para os conectivos; esta parte deve ser uma solução fácil.

2. Um pouco mais complicada é a rotina de exportação no userio.js; a sintaxe do fitchpacote é substancialmente diferente da sintaxe para adicionar uma linha de prova no lplfitchpacote e exigirá um pouco mais de tempo para reescrever.

   (Parece que a prova está armazenada internamente em uma pilha (se minha análise superficial estiver correta); nesse caso, pode ser melhor descartar a rotina de exportação existente e escrever algo novo, que se baseia na conversão das provas primeiro em linhas e em seguida, converter linhas individuais (incluindo o número correto de barras verticais) em uma linha na saída, ignorando completamente a estrutura lógica. Isso é totalmente o oposto do que lplfitchdeseja.)