LaTeX 백엔드를 사용한 Fitch 스타일 증명을 위한 최소 WYSIWYG 프로세서

Question

이것이 TeX.SE 또는 Stackoverflow에 더 적합한지는 잘 모르겠지만 대부분 TeX 중심이라는 점을 고려하면 여기서는 TeX 하이브 마인드가 가장 적합할 것이라고 생각했습니다.

저는 피치 스타일의 논리 증명을 작성하기 위한 GUI 문서 프로세서를 갖고 싶습니다.LPLFitch 패키지. 나는 사용자가 TeX 코드와 직접 상호 작용할 필요 없이 백엔드에서 LaTeX를 사용하여 완전히 WYSIWYG(보이는 대로 얻는 것)이기를 원합니다. 또한 사용자 컴퓨터에 LaTeX를 설치할 필요 없이 완전히 독립적으로 작동하고 싶습니다. TeX 경험이 없는 학생들이 그러한 증명을 생성하는 데 도움이 될 것입니다.

내가 가진 질문은 기존의 오픈 소스 리소스가 무엇입니까? 내가 아는 유일한 종류의 것은릭스, 그러나 이는 내가 염두에 두고 있는 최소한의 프로세서와는 반대로 LaTeX의 전체 규모 구현을 목표로 합니다. 이는 매우 적은 수의 패키지와 LaTeX의 전체 기능 중 최소한의 하위 집합만 활용합니다.

목표:

1. 완전히 WYSIWYG인 문서 프로세서입니다.
2. 필요한 기호를 삽입할 수 있는 몇 개의 버튼이 있고 해당 기호를 즉시 렌더링합니다(유니코드 기호로 삽입하거나 빠른 컴파일 실행을 통해).
3. 사용자 측에서는 LaTeX에 대한 지식이 필요하지 않으며 사용자 컴퓨터에 전체 LaTeX 설치가 필요하지 않습니다.
4. LPLFitch 패키지와 같은 Fitch 스타일의 자연 추론 증명을 생성합니다.

질문:

1. 내가 구축할 수 있는 기존 오픈 소스 리소스는 무엇입니까?
2. 이와 같은 것을 처음부터 구현하는 데 어떤 조언을 해주실 수 있나요(예: LuaTeX 또는 좀 더 프로그래밍 방식의 TeX 사용)?
3. 이것이 좋은 생각일까요, 아니면 LaTeX에 익숙하기 때문에 더 나은 솔루션을 찾을 수 없게 되는 것일까요?

나는 이것이 매우 개방적이고 미개발된 질문이라는 것을 알고 있습니다. 이제 막 시작하는 아이디어이고 경험도 많지 않지만 꼭 해보고 싶은 프로젝트입니다. 질문이 현재 형식의 사이트에 적합하지 않은 경우 충분히 이해합니다.

Answer 1

두 개의 웹 기반 서비스는 질문에서 묻는 것과 거의 유사한 작업을 수행합니다. 두 경우 모두 서비스는 일종의 TeX 내보내기를 지원합니다. 그러나 lplfitch원래 질문에서 참조된 패키지를 사용하지 마십시오.

• 피치JS(또한보십시오라이브 버전)는 Johan Klüwer의 패키지를 사용하여 형식으로 내보냅니다 fitch.sty. (사본은 다음에서 구할 수 있습니다.로직매터스프로젝트의 Git 저장소에도 있습니다 fitchjs.)
• 증명자체적으로 출력맞춤 형식; 하지만 그들의 코드가 오픈 소스인지는 확실하지 않습니다. (또한 영어판에 비해 한국어판이 개발이 더 활발한 것 같습니다.)

FitchJS포크 하여 사용하는 것이 가능합니다 lplfitch. LaTeX 생성을 처리하기 위한 코드는 두 개의 파일에 있습니다.

1. parsing.js유니코드 기호가 LaTeX 등가물과 번역되는 부분이 있습니다 . lplfitch연결에 대해 다른 마이크로를 사용합니다. 이 부분은 쉽게 고쳐질 것입니다.

2. 의 내보내기 루틴은 약간 더 복잡합니다 userio.js. 패키지의 구문은 패키지 fitch에 교정 줄을 추가하는 구문과 크게 다르며 lplfitch다시 작성하려면 조금 더 많은 시간 투자가 필요합니다.

   (증명은 내부적으로 스택에 저장되어 있는 것으로 보입니다(내 피상적인 보기가 정확하다면). 이 경우 기존 내보내기 루틴을 덤프하고 새로운 것을 작성하는 것이 더 나을 수 있습니다. 이는 먼저 증명을 라인으로 변환하고 그런 다음 논리적 구조를 완전히 무시하고 개별 줄(정확한 수직 막대 수 포함)을 출력의 한 줄로 변환합니다. 이는 lplfitch원하는 것과 완전히 반대입니다.