ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] new logic

 To: cmenzel@xxxxxxxx, "[ontolog-forum]" Adrian Walker Tue, 19 Jan 2010 19:03:35 -0500 <1e89d6a41001191603y7ba0393ct6fba1efdbd0f1b21@xxxxxxxxxxxxxx>
 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.                            Cheers,  -- AdrianInternet Business LogicA Wiki and SOA Endpoint for Executable Open Vocabulary English over SQL and RDFOnline at www.reengineeringllc.com    Shared use is free, and there are no advertisements Adrian WalkerReengineeringOn Tue, Jan 19, 2010 at 6:38 PM, Christopher Menzel wrote: On Tue, 2010-01-19 at 13:36 -0500, Patrick Cassidy wrote: > John, >    Re: Describing a computation with FOL >    Can FOL actually *perform* arithmetic functions? That's like asking whether English can dance the tango.  FOL doesn't *do* anything.  FOL is a language, a semantics and (typically) a system by means of which an agent can generate proofs.  Thus, FOL can be *used* to represent information and demonstrate, e.g., when one thing follows from another.  You can therefore *describe* a computation in FOL and prove things about that computation.  But FOL of itself doesn't do anything at all. > I know that one can assert that there is a function that takes two > numbers and associates with them their sum, but it seems that to use > such a function in FOL one needs to have a preexisting table of such > sums, impractical in the general case.  Is there a way for FOL > reasoning to actually **compute** a sum (or difference, product, > ratio) as a Turing machine could? Well, now you've changed the subject from FOL to FOL *reasoning*.  And, under one reasonable interpretation of "FOL reasoning", the answer is "yes".  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. Chris Menzel *This is in fact how one shows that the undecidability of first-order logical implication follows from the halting problem. For details, see Boolos, Burgess, and Jeffrey, Computability and Logic, ch 11. _________________________________________________________________ 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 ``` _________________________________________________________________ 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    (01) ```
 Current Thread Re: [ontolog-forum] new logic, Rob Freeman Re: [ontolog-forum] new logic, Paola Di Maio Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Paola Di Maio Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, Patrick Cassidy Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, Adrian Walker <= Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, Patrick Cassidy Re: [ontolog-forum] new logic, Jakub Kotowski Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Patrick Cassidy Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Rich Cooper Re: [ontolog-forum] new logic, Rob Freeman Re: [ontolog-forum] new logic, Paola Di Maio Re: [ontolog-forum] new logic, John F. Sowa