This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic.
K. Heng. (2014)cite arxiv:1404.6248Comment: Published in American Scientist: Volume 102, Number 3, Pages 174 to 177 (http://www.americanscientist.org/issues/pub/2014/3/the-nature-of-scientific-proof-in-the-age-of-simulations).
H. Cao, and X. Zhu. (2006)cite arxiv:math/0612069Comment: This is a revised version of the article by the same authors that originally appeared in Asian J. Math., 10(2) (2006), 165--492.
E. Stark. Foundations of Software Technology and Theoretical Computer Science, volume 206 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, (1985)
J. Søgaard-Andersen, S. Garl, J. Guttag, N. Lynch, and A. Pogosyants. PROCEEDINGS OF THE 5TH INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION, ELOUNDA, GREECE, VOLUME 697 OF LECTURE, page 305--319. Springer Verlag, (1993)