Automated Reasoning for Second-Order Formalisms

Second-order logics are logics where the quantifiers do not only quantify elements of the domain but are also allowed to quantify sets of elements and relations over elements. Such quantification make second-order logics very expressive but also very complex and highly undecidable. In general, reasoning is second-order logic is deductively incomplete. Nevertheless, second-order formalisms are very useful and more and more applications focus interest on second-order formalisms.
Often it is mathematically possible to eliminate second-order quantifiers. Research can be undertaken to use second-order quantifier elimination methods to develop and study methods for techniques for automated correspondence theory of modal logic; automated reasoning in second-order modal logic (e.g. reasoning about the equivalence of axioms and rules, knowledge compilation or non-monotonic reasoning); and automated reasoning in fragments of second-order logic, for example the monadic fragment, for various applications.