This file is the written thesis. Be warned, it's written in Polish.
This directory contains all LaTeX code and resources used to write the paper.
This directory contains the code of the application. To run it, open the index.html file in your browser.
This directory contains an implementation of the application in Prolog, and a README file with instructions on how to run it.
WARNING: The translation below was done automatically and thus might contain some errors.
Web application for proving tautologies in set theory The goal of this paper was to create a simple and intuitive tool for proving tautologies in set theory. This was accomplished in a web application using pure HTML, CSS and JavaScript. The basics of set theory, their relationship with logic, and methods for proving tautologies were described. The way the application works, reverse polish notation, interesting code fragments, and conclusions about the implementation are discussed.
The aim of the work was to design and implement a web application for verifying tautologies in set theory. In other words, the application checks whether a given sentence is logically true. The application created as part of the work was supposed to have a user-friendly interface, similar to a calculator, and potentially serve as a didactic aid. Another goal of the work was to present the connection between logic and set theory and provide an opportunity to learn. The theoretical foundations described in the previous chapters, the algorithms designed based on them, their implementation in code, and the application screens allow us to conclude that this goal has been achieved.
The work proposes a tabular method for numerically verifying tautologies. This means that for the entered sentence, a table of all possible logical values of this sentence is generated, depending on the logical values of its components. The application consists of three screens. The first one is a calculator screen used to enter the sentence and display the result as true or false, indicating whether the sentence is a tautology or not. The second screen contains a visualization of the table generated by the program. The third screen is static and shows how set operations translate into logical operations.
One of the main difficulties in creating this application was the possibility of allowing the user to enter any sentence with any set operations. Checking a specific sentence using code is much simpler.
The aim of the work was to design and implement a web application for verifying tautologies in set theory. In other words, the application checks whether a sentence provided by the user is always logically true. The application was supposed to have a user-friendly interface in the style of a calculator and potentially serve as a teaching aid. Another goal of the work was to present the connection between logic and set theory and provide an opportunity for learning. The theoretical foundations described in previous chapters, algorithms designed based on them, their implementation in code, and application screens allow us to conclude that this goal has been achieved. The method proposed in the work for numerically verifying tautologies is the table method. This means that for the entered sentence, a table of all possible logical values of this sentence is generated, depending on the logical values of its components. The application consists of three screens. The first one is the calculator screen used to enter the sentence and display the result in the form of true or false, indicating whether the sentence is a tautology or not. The second screen contains a visualization of the table generated by the program. The third one is static and shows how set operations translate into logical operations. One of the main difficulties in creating this application was the possibility for the user to enter any sentence with any set operations. Checking a specific sentence with code is much easier.
The table method used, despite its simplicity, is very inefficient in terms of memory, even if, as in this application, logical values are stored on individual bits. This is due to the fact that the program has exponential memory complexity, i.e. if the checked sentence has n sets, the generated table has 2^n rows. Furthermore, although the maximum number of sets that can be entered is equal to the number of keys on the keyboard, and therefore the number of rows is limited, the number of columns can theoretically be infinite. This is because the table has columns for each operation contained in the given sentence, but no restrictions have been introduced regarding its length. Another problem is generating the view and displaying the table created by the program. For a large number of sets, the table screen takes a very long time to generate, and trying to open it can crash the browser.
This situation has never occurred for a calculator screen, but the time it takes to obtain the result for very long sentences can reach even several dozen seconds.
There are several potential ways to solve this problem. Since the sentence is not a tautology, if it is false in at least one case, instead of generating and checking the entire table at once, for longer sentences, it can be checked fragmentarily.
Similarly, the situation is the same when generating and displaying its view. Then the user would have to have the ability to manually instruct the application to display the remaining part of the table.
Additionally, there are easier ways to implement a truth table proof. One of them is to use the PROLOG language. With its help, a similar program can be created much more easily. As part of this work, a preliminary version of the program was created in this language, limited in terms of available operations. Launched in the SWI-Prolog environment, it generated the table created during the calculations and returned the correct result in the form of true or false. However, this application was not created in full, so it was not determined whether it is faster compared to the created solution. Additionally, using the PROLOG language would require creating an additional user-friendly interface because in its basic version, it is difficult to use.
The program described above that uses PROLOG still uses the truth table method. The author is not aware of any other methods of numerically proving tautologies in set theory. Therefore, the basic improvement of the created application would be to search for other, more optimal ways of proving tautologies and their implementation, while maintaining the current interface. In case no alternatives are found or their implementation is impossible, one can try to create an application from scratch using PROLOG and compare its execution times. For the application in its current form, since it is intended as a potential educational aid, it is worth creating additional views that better explain its operation, such as presenting the process of converting the sentence provided by the user to the Reverse Polish Notation.