[Top] [All Lists]

Re: [ontolog-forum] new logic

To: Adrian Walker <adriandwalker@xxxxxxxxx>
Cc: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 19 Jan 2010 19:02:13 -0600
Message-id: <1263949333.5096.52.camel@new-philebus>
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)

<Prev in Thread] Current Thread [Next in Thread>