The FOL Evaluator is a semantic calculator which will evaluate a well-formed formula of first-order logic on a user-specified model. In its output, the program provides not just the formula's truth value, but also a description of the entire evaluation process used to determine that truth value. If you come across any bugs, please email me at mrieppel at gmail dot com.
A live version of the program is here.
(c) Michael Rieppel 2012-2017. Released under the MIT License. See LICENSE for more information.