 Theorem-provers developed for higher-order logics, working from a variety of approaches, include TPS (Andrews and Brown 2006), Leo-II and -III (Benzmüller, Sultana, Paulson, &amp; Theiß 2015; Steen &amp; Benzmüller 2018), and perhaps most prominently HOL and particularly development-friendly  Isabelle/HOL  (Gordon &amp; Melham 1993; Paulson 1990). With clever implementation and extension, these also allow automation of aspects of modal, deontic, epistemic, intuitionistic and paraconsistent logics, of interest both in their own terms and in application within computer science, robotics, and artificial intelligence (McRobbie 1991; Abe, Akama, &amp; Nakamatsu 2015).