This project is aimed at developing a program to evaluate the truth-value of sentences in First-Order Logic and construct proofs.