From rspeer@MIT.EDU Tue Aug 24 14:46:22 2004 Received: with ECARTIS (v1.0.0; list lojban-beginners); Tue, 24 Aug 2004 14:46:22 -0700 (PDT) Received: from fort-point-station.mit.edu ([18.7.7.76]) by chain.digitalkingdom.org with esmtp (TLS-1.0:DHE_RSA_3DES_EDE_CBC_SHA:24) (Exim 4.34) id 1Bzj7W-0008Mm-DC for lojban-beginners@chain.digitalkingdom.org; Tue, 24 Aug 2004 14:46:22 -0700 Received: from grand-central-station.mit.edu (GRAND-CENTRAL-STATION.MIT.EDU [18.7.21.82]) by fort-point-station.mit.edu (8.12.4/8.9.2) with ESMTP id i7OLkMTA022691 for ; Tue, 24 Aug 2004 17:46:22 -0400 (EDT) Received: from melbourne-city-street.mit.edu (MELBOURNE-CITY-STREET.MIT.EDU [18.7.21.86]) by grand-central-station.mit.edu (8.12.4/8.9.2) with ESMTP id i7OLkLFA006047 for ; Tue, 24 Aug 2004 17:46:21 -0400 (EDT) Received: from torg.mit.edu (TORG.MIT.EDU [18.208.0.57]) ) by melbourne-city-street.mit.edu (8.12.4/8.12.4) with ESMTP id i7OLkIpq023246 for ; Tue, 24 Aug 2004 17:46:20 -0400 (EDT) Received: from rob by torg.mit.edu with local (Exim 3.36 #1 (Debian)) id 1Bzj7j-0002sm-00 for ; Tue, 24 Aug 2004 17:46:35 -0400 Date: Tue, 24 Aug 2004 17:46:35 -0400 From: Rob Speer To: lojban-beginners@chain.digitalkingdom.org Subject: [lojban-beginners] Re: logical proofs? Message-ID: <20040824214635.GA10772@mit.edu> Mail-Followup-To: lojban-beginners@chain.digitalkingdom.org References: <1093232310.412966b640996@www.gulik.co.nz> <20040823041958.GD3257@chain.digitalkingdom.org> <20040823031849.A32026@fresco.Math.McGill.CA> <20040823153053.GI3257@chain.digitalkingdom.org> <1093296583.412a61c7e09ce@www.gulik.co.nz> <20040823214759.GE3257@chain.digitalkingdom.org> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20040823214759.GE3257@chain.digitalkingdom.org> X-Is-It-Not-Nifty: www.sluggy.com User-Agent: Mutt/1.5.6+20040523i X-archive-position: 733 X-Approved-By: rspeer@MIT.EDU X-ecartis-version: Ecartis v1.0.0 Sender: lojban-beginners-bounce@chain.digitalkingdom.org Errors-to: lojban-beginners-bounce@chain.digitalkingdom.org X-original-sender: rspeer@MIT.EDU Precedence: bulk Reply-to: lojban-beginners@chain.digitalkingdom.org X-list: lojban-beginners On Mon, Aug 23, 2004 at 02:47:59PM -0700, Robin Lee Powell wrote: > > What I'm interested in is whether it is possible that this could be > > mechanically derived, for example by somebody using a proof assistant > > such as COQ, but using lojban? I.e are all the steps in the proof > > mechanical enough to convince a computer that (e.g.) prime numbers are > > infinite? > > Rob Speer is working on something like this. Rob? I haven't thought of using my system as a proof assistant. I don't think doing so would be especially useful - it would basically just be an awkward frontend to something like COQ. My main goal is for my system to do common-sense reasoning, not mathematical reasoning, because there already is a language perfectly suited for doing mathematical proofs - the language of math. -- Rob Speer