(The following probably isn't very useful in any practical way. but I'll
add it to the accumulated list knowledge just in case.)
Determining whether a system of statements in (for example) first-order
logic is true is a well-solved problem by Analytic Tableaux. For a start,
see http://en.wikipedia.org/wiki/Tableau_method
This elegant method is expressible in Prolog in four simple rules,
requiring little more than that number of lines of code. Maxima doesn't
include a Prolog engine, of course, but the Tableau method could be
implemented in Common Lisp in a very small body of code. But this probably
isn't an appropriate solution for the OP's needs.