Skip to main content

Researching the Problem

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

Comments

Post a Comment

Popular posts from this blog

Background Information

     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...
Post a Comment
Read more

Starting the 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.
Post a Comment
Read more

End Result

I am now finished working on my project for the semester. I ended up with something that I am okay with, but I think I would have liked it to be better than it is. But because of the time constraints, I tried to make it as good as possible with the time that we had. Right now the input to my program is the string that you want to prove and the output is a tex file that produces a pdf of the proof. I decided to do this because math symbols are much easier to read this way rather than trying to express them with normal characters. My program can only handle very simple proofs, so something I would like to change if I had more time would be to test more cases and make adjustments for my program to be able to prove more complex theorems. I have included an example output from my program.
Post a Comment
Read more