First-Order Logic with Natural Deduction (constructive and classical versions). For a classical sequent calculus, see Isabelle/LK. Useful references on First-Order Logic: Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991) (The first chapter is an excellent introduction to natural deduction in general.) Antony Galton, Logic for Information Technology (Wiley, 1990) Michael Dummett, Elements of Intuitionism (Oxford, 1977)
Examples for First-Order Logic.