About This Application

This application is developed to facilitate the creation of proof diagrams known as natural deduction, as introduced by Gentzen. Through an intuitive graphical user interface, users can efficiently generate diagrams and export them in LaTeX format.

For individuals unfamiliar with LaTeX syntax, this tool provides an accessible means to convert GUI-constructed diagrams into TeX code. The diagrams generally encompass premises and conclusions, interconnected by a series of logical steps. When a premise is established, it is assigned a unique identifier, enabling easy selection and reuse during the logical derivation process.

Additionally, the application is equipped to identify errors within proof constructions that might otherwise lead to infinite recursion. This is achieved by tracking the logical path back to the problematic premise. A real-time LaTeX rendering view is also available, allowing users to address potential errors proactively before the compilation phase. Furthermore, those unfamiliar with TeX can benefit from our automatic LaTeX insertion, simply by clicking designated buttons referred to as "Rules".

We anticipate that this application will serve as a valuable resource for students within mathematics and information technology disciplines, enhancing both their learning and productivity.

This application is licensed under the MIT License. © 2025 Kengo Saito. Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.