The RAIR Lab and affiliates are responsible for a large amount of graphical interactive theorem proving software. Graphical Interactive Theorem Provers (GITPs) provide a theorem proving environment with a robust UI and visualization tools that allow for ease of proof construction above regular the text based interactive theorem provers.

The RAIR Lab’s main work in this area has been the Slate family of GITPS. These provide directed-acyclic-graph based representation for natural-deduction based inference systems in a variety of logics including propositional, first-order, higher-order, and modal logics.

The RAIR Lab also maintains PMH, a powerful graphical interactive theorem prover for Charles Sanders Peirce’s Alpha Existential Graph system.