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 (01)
Powerful, you say? (02)
Anyway, two things: (03)
1) Tau has two authors, Jay Halcomb and myself
(in the guise of H&S Information Systems).
2) Otter has been superceded in development by Prover9
(<http://www.cs.unm.edu/~mccune/mace4/>) (04)
Randall Schulz (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)
|