Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!mnetor!uunet!husc6!bloom-beacon!gatech!hubcap!steve
From: steve@hubcap.UUCP ("Steve" Stevenson)
Newsgroups: sci.philosophy.tech
Subject: Re: What is a methodology
Message-ID: <409@hubcap.UUCP>
Date: Tue, 25-Aug-87 09:12:40 EDT
Article-I.D.: hubcap.409
Posted: Tue Aug 25 09:12:40 1987
Date-Received: Wed, 26-Aug-87 06:24:53 EDT
References: <152@aiva.ed.ac.uk>
Organization: Clemson University, Clemson, SC
Lines: 16

in article <152@aiva.ed.ac.uk>, jeff@aiva.ed.ac.uk (Jeff Dalton) says:
> There have > been attempts to develop an inductive logic, effectively to
> do science automatically, and they have failed.  We can't even do deduction
> (as in > automatic theorem proving) fully automatically.  Mathematics is still
> "creative" and likely to remain so.

The problem with both of the above is the power of the model with which you
are trying to use in "automating" the proofs.  I think you are using
creative in two senses: *de novo*, and *to solve in a non-Turing computable
way*.  I think "inductive" here is the *de novo* sense.  Since the Herbrand
procedure is a semi-decision procedure, we're "half way" there :->.

-- 
D. E. (call me Steve) Stevenson            steve@hubcap.clemson.edu
Department of Computer Science,            (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906