On 2013-12-13, Steve Haflich <shaflich at gmail.com> wrote:
> 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.
I am a big fan of declarative programming -- I have sometimes
entertained the idea that Maxima could implement something like Prolog
or a subset of it. The syntax need not be the same, but maybe some of
the same functionality could be useful and interesting.
FWIW
Robert Dodier