On Mon, Sep 17, 2007 at 06:57:05AM -0700, Randall R Schulz wrote:
> On Sunday 16 September 2007 20:36, Chris Menzel wrote:
> > On Sun, Sep 16, 2007 at 10:23:08PM -0500, Chris Menzel wrote:
> > > ...But that isn't to say that nothing can be done
> > > within those limitations if a problem turns out to be NP-complete
> > > or even (in general) undecidable -- consider, e.g., full
> > > first-order reasoners like Otter.
> >
> > Or, I should have added, Randall Schulz's powerful Tau theorem
> > prover (which implements a dialect of Common Logic).
> >
> > -chris
>
> Powerful, you say?
>
> Anyway, two things:
>
> 1) Tau has two authors, Jay Halcomb and myself
> (in the guise of H&S Information Systems). (01)
Oops, yes, my apologies to Jay. Long day... (02)
> 2) Otter has been superceded in development by Prover9
> (<http://www.cs.unm.edu/~mccune/mace4/>) (03)
Yes, in fact I was going to cite Prover9 for that very reason but
figured Otter was a more familiar name. (04)
-chris (05)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (06)
|