OtterFace-8

OtterFace-8 is a simple graphical user interface for Otter and Mace2. (an automated deduction system which is designed to prove theorems stated in first-order logic with equality).

It doesn't help you prepare input to Otter/Mace2. You still have to know the input language and prepare input files with your favorite plain text editor.