Isabelle/FOL sessions

FOL

    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)
  
FOL-ex

    Examples for First-Order Logic.