CSIT 441 Semester Project

I have started programming my project. I decided that I was going to do this in java and make everything from scratch. To make the math symbols look better, I decided to have my program generate a laTex file with the theorem and the proof. This makes the end result a lot easier to read. So far I have been working on coming up with a bunch of different test cases so I can make my program work with as many special cases as possible. What I have left to work on is implementing these cases and trying to come up with code that will work as generally as possible. I'm sure that I will run into some problems along the way with this. But what I have done so far has been going pretty well. So, hopefully the rest will go as smoothly.

Over the past week I have worked on learning more about Automated Theorem Proving. I have been trying to come up with a plan and have been doing this by reading what other people have posted about solving problems like this. I am still not quite sure where to start with this project, so I am hoping that after reading more about it that I will be able to get a good start on it within the next few days. I have read a lot about people solving these types of problems using neural networks, so I think that will probably be the best way to go with this project. I will have to research this a lot more and figure out the best approach to solving this problem. References: http://www.cs.miami.edu/~tptp/OverviewOfATP.html https://cs.stanford.edu/people/eroberts/courses/soco/projects/1999-00/automatic-theorem-proving/theory.htm

     For my semester project in Artificial Intelligence I plan on writing a program that will be able to solve simple math theorems. I plan on working with more simple proofs like proofs involving the equality of sets and proofs by induction. I think that working with these will be the best option because they are the easiest types of proofs and I am hoping that because they are all very similar that they will be the easiest to implement.      Currently, there is a debate as to whether computers will be able to solve the very complex proofs that require a lot of reasoning. Many mathematicians believe that computers will never be able to do this better than humans just because of how much logic and reasoning is necessary to prove certain theorems. An example of the types of Theorems I would like to be able to prove with this program would be DeMorgan's Law. Which states that ㄱ(A ∧ B) = ㄱA  ∨ ㄱB and ㄱ(A ∨ B) = ㄱA ∧ ㄱB. Sources: http://www.slate.c...