books.google.es - This graduate-level text presents fundamental concepts and results of classical logic in a rigorous mathematical style. Applications to automated theorem proving are considered and usable Prolog programs provided. It will serve both as a first text in formal logic and an introduction to automation issues...http://books.google.es/books/about/First_Order_Logic_and_Automated_Theorem.html?hl=es&id=nYN0dBrCpmMC&utm_source=gb-gplus-shareFirst Order Logic and Automated Theorem Proving
