This project aims to investigate the undecidability of first order logic (FOL) by converting a Turing Machine into FOL statements.
Due to technical limitations of our ability, the program is currently only usable in the command line. Type make into your terminal once you've navigated to the folder this project resides.
To use the program you would need to prepare the following two files:
- A
.xmlfile representation of the Turing Machine, you can generate this file by clicking "Save XML" in the Turing Machine Software. - A
.txtfile representation of the Turing Machine Tape, you can generate this file by clicking "Save Tape" in the Turing Machine Software.
Use the command ./tm-to-fol turing-machine.xml turing-machine-tape.txt to run the program. After the program has terminated, you will be able to find turing-machine.bram in your folder. This will be the First Order Logic statements that describe the Turing Machine along with its tape you have put in.
You could include an extra parameter at the end of the command to indicate which cell the initial read write head is located at (default value is 0, i.e. the leftmost cell of the tape).
The output file of this program follows the Bram File Format and can be viewed using Aris. Note that even with small Turing machines, the output file can contain a lot of symbols which will take some time for Aris to load.
- Due to the inability to represent negative integers, this program can only translate Turing Machines with the assumption that the read-write head will never move to the left of its initial position. If it does, it will just go back to its initial position.
For those who are taking Computability and Logic and wanting to contribute to project. Here are possible improvements one could make to the program:
- Creating a Graphical User Interface
- Coming up with a way to represent the integers (both positive and negative) in formal logic so we don't have to restrict ourselves with machines using single-sided infinite tapes.