A: The delay you experience is because I used
to develop the page. If you know some web development, Right-click > View source code
on any of the site's excercise pages and you will se what i'm talking about.
A: Then you might want to check out
Reconstructor's base language allows you to define a first-order language with
indefinitely many constants, predicates, variables and even function symbols. It also contains
arithmetic, set theory and other mathematics inside the object language.
A: For classical logic (and intuitionist and minimal natural
deduction systems), you may see L.T.F. Gamut (1991) Logic, language and meaning
(there is a spanish translation available). For the non-classical multivalued logics of
the FDE family, see Priest (2008) An Introduction to Non-Classical Logic in
english, Da Ré & Roffé (2016) Introducción a las Lógicas Modales y No-clásicas in
spanish. For the logics with consistency (or inconsistency) operators inside the object
language (such as LFI1), see Carnielli & Coniglio (2016) Paraconsistent Logic.