Turnstyle is an attempt to fill a gap in currently available software in computational logic.  There are no standardised libraries of routines for predicate logic, forcing each programmer to generate new routines for each program.  Turnstyle is a carefully designed library of routines that will be open-sourced, so that anyone who wishes may use them.  The current version of Turnstyle accepts formulae and determines whether a given formula is well-formed or not.  When I finish Turnstyle, it will become the core of a modern proof verification program.  Here is a prototype interface I am using for testing the Turnstyle framework:

PCLogic is a Windows-based proof verification program for formal derivations in sentential logic, monadic predicate logic, and polyadic predicate logic with identity. It is designed to give students feedback on each step of a derivation, flagging errors either immediately, or in a delayed mode to simulate testing.  PCLogic is not currently being developed, but is available for trial and purchase.

PCLogic uses a Lemmon-Gentzen style system of natural deduction, consisting of introduction and elimination rules for the standard operators and quantifiers (ampersand, arrow, tilde, wedge, universal, existential), a definition rule for the double-arrow, introduction and elimination rules for the identity predicate (=), and a theorem introduction rule. This system and its variants are quite popular, allowing PCLogic to be used in conjunction with a variety of introductory logic texts, including Forbes's Modern Logic, Goldfarb’s Deductive Logic and Lemmon’s Beginning Logic.