Programming First-Order Logic So I recently started reading about logic, and I have decided to try to implement the subject in my final project for a mathematical programming class I am taking.  I wasn't going to try to make anything too advanced or anything, but I figured it would be a good learning experience as well as an interesting project.
Of course, I don't have much experience with logic.  I've been learning about it as I go, but there are plenty of concepts about which I haven't a clue.  So, I was hoping you may be able to point me in the direction of where I should go in order to learn the minimum for completing my project.
Ideally, I was going to make a proof checker of first order logic.  I wanted to give it a string of first-order logic symbols, and have it check if it could have been deduced from a set of axioms I gave it.  I was thinking about writing it so that it resembles the system set up by Gödel in his proof of the incompleteness theorems, but I'm not sure if that is feasible.
I was able to make a program that takes in a statement of propositional logic and return whether or not it was true or not, but I'm not sure if I did it 'right,' and adding things like existential quantifiers has stopped me in my tracks.
So, I think I can program it.  I just need to know what I'm programming.  If I'm missing something here, please let me know.  I'd hate to start this project then find out in a couple of weeks that I'm missing some fundamental pieces of information that will prevent me from completing it.
Any help is appreciated.
 A: 
I was able to make a program that takes in a statement of propositional logic and return whether or not it was true or not, but I'm not sure if I did it 'right,' and adding things like existential quantifiers has stopped me in my tracks.

With good cause, since logical validity in first-order logic is known to be undecidable -- it is impossible, even in principle, for a program to decide correctly whether an arbitrary first-order sentence is logically valid or not.
What does exist, to various degrees of sophistication, is proof checkers and theorem provers. A proof checker takes not only a conclusion, but also a purported proof of it, and determines whether the proof is correct or not. The chief challenge in constructing one is finding a notation for proofs which is simple, complete, and also natural enough that short (or at least not horribly long) proofs of interesting sentences can be written by hand reasonably naturally. A Hilbert-style proof system such as the one Gödel wrote about is not going to cut it in practive -- at a minimum you'll want to use a system where the Deduction Theorem is a primitive rule, such as some appropriate syntax for Natural Deduction.
A theorem prover works autonomously, given just the conclusion you want it to prove, but on the other hand it will not always be able to find a proof even if one exists. A lot of ingenuity and heuristics have gone into constructing them over the years, but they still work best in relatively sheltered contexts where they can be based on domain knowledge in addition to just logic, such as certain subsets of arithmetic.
As a toy project, an automated theorem prover would sound very ambitious -- you would have to restrict yourself to a very narrow range of possible theorems, and even finding an interesting one could require a lot of literature study.
Proof checkers are more well understood -- the rules are what they are, after all -- and you'd have some chance of getting proofs for some simple, yet not completely trivial, theorems checked at the end of the day.
