On Tue, 2010-01-19 at 19:03 -0500, Adrian Walker wrote:
> Hi Chris --
>
> You wrote..
>
> For a given Turing machine M halts on input n if and only if
> there is a corresponding proof in first-order logic that in a precise
> sense represents M's computation.* Hence, by means of first-order
> reasoning one can compute a sum, difference, product, ratio etc just
> as a Turing machine could -- however, typically it would be a lot
> quicker and easier just to perform a simple arithmetic proof directly
> using, say, Peano Arithmetic.
>
> Yes indeed, FOL plus an inference engine can do (integer)
> arithmetic.
>
> However, in all of the practical logic-based systems I'm aware of,
> arithmetic is actually done by "built in predicates", aka calls to
> traditional libraries coded in C, Java or such. (01)
Well sure, Adrian, but practicality was not the issue as I understood
it. The question was simply whether there was any sense in which
"first-order reasoning" could perform a computation "as a Turing machine
could". I wouldn't recommend doing pure FOL theorem proving (i.e.,
without the benefit of "traditional libraries") for doing practical
mathematical computing any more than I'd recommend using an actual
Turing machine. :-) (02)
-chris (03)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (04)
|