On Sep 28, 2008, at 2:51 PM, Adrian Walker wrote:
In general, however, the problem of determining when one thing follows from
another is undecidable (hence intractable). So a serious challenge of
AI is to figure out how to do useful reasoning in the face of this
One approach to this is of course to choose a subset of formal logic that is (a) useful for AI, (b) decidable, and (c) has tractable complexity on current computers.
Thanks for the references, Adrian. As you note, that is indeed the central strategy of logic-based AI for dealing with the challenge of undecidability, point (a) especially being the kicker.
The paper  and the system  represent one set of choices in this area. No doubt there are many others.
Notably, in addition to your work, all the work on description logics, which serve as the foundation for OWL (more exactly OWL-DL -- see http://dl.kr.org
 Backchain Iteration: Towards a Practical Inference Method that is Simple Enough to be Proved Terminating, Sound and
Complete, A. Walker. Journal of Automated Reasoning, 11:1-22.
 Internet Business Logic
A Wiki and SOA Endpoint for Executable Open Vocabulary English over SQL and RDF. Online at
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (01)