On Fri, Dec 13, 2013 at 06:34:10PM +0000, Robert Dodier wrote:
> 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
> >
"well-solved problem" ?? It's undecidable, just to remember, and thus it
depends enormously on which special cases are considered, what
algorithms are used, and how it is implemented.
It seems rather alarming that the mentioned Wikipedia page doesn't
mention the word "undec*".
> > This elegant method is expressible in Prolog in four simple rules,
> > requiring little more than that number of lines of code.
This likely wouldn't help except in the most trivial cases.
Thus I would be rather careful here.
An implementation in Prolog is just a student project, to play around
with Prolog.
Oliver