Path: utzoo!attcan!uunet!lll-winken!lll-tis!helios.ee.lbl.gov!pasteur!ucbvax!decwrl!labrea!glacier!jbn
From: jbn@glacier.STANFORD.EDU (John B. Nagle)
Newsgroups: comp.ai
Subject: Re: Rules vs axioms
Message-ID: <17694@glacier.STANFORD.EDU>
Date: 10 Sep 88 15:17:45 GMT
References: <3546@s.cc.purdue.edu> <2365@uhccux.uhcc.hawaii.edu> <918@l.cc.purdue.edu> <14108@agate.BERKELEY.EDU>
Reply-To: jbn@glacier.UUCP (John B. Nagle)
Organization: Stanford University
Lines: 12


     In theorem proving, previously proved theorems are often used, correctly,
as rewrite rules.  Free addition of new "axioms" to theorem proving systems
generally results in unsoundness.  As Boyer and Moore once wrote, "It is
one thing to use axioms about a concept known to mathematics for
a century.  It is quite another to write down axioms about an idea
invented yesterday."   See Boyer and Moore's "A Computational Logic"
for the constructivist's way of avoiding this problem.

     Attempts to use the theorem proving paradigm in less formal domains 
were made in the late 70s and early 80s, but without notable success.

					John Nagle