Re: SUO: a silly question about the new modular architecture
Adam,
Amazing. We finally agree.
John
Adam Pease wrote:
>
> John,
> I'm happy with this (thought it might never happen, eh? :-). This is a
> clear operational definition for a type of theory merging that can be
> performed with existing tools. Thank you.
>
> Adam
>
> At 10:39 AM 9/1/2001 -0400, John F. Sowa wrote:
> >Adam,
> >
> >Theory compilation is trivial. The tools to do it come for free
> >with every Unix system. (And there are Unix-like tool packages
> >that can also be run on legacy systems, such as Windows.)
> >
> > > I don't believe that there are any existing tools that would perform
> > > this sort of theory compilation nor has anyone volunteered to build them
> > > but that's another story.
> >
> >Given the axioms for theory A and the axioms for theory B,
> >you can create the axioms for the combined theory C
> >by using the cat (concatenate) command in Unix:
> >
> > cat A B > C
> >
> >This creates a new file C, which contains all the axioms for
> >both A and B.
> >
> >There are now two more questions one would like to ask:
> >
> > 1. Is the new theory consistent?
> >
> > 2. Are any of the axioms redundant?
> >
> >Both questions can be answered by running your favorite theorem
> >prover. To answer #1, try to derive a contradiction (i.e., the
> >empty clause in resolution theorem provers). That is a test that
> >should be performed on any theory, especially if it was produced
> >by hand coding.
> >
> >To answer #2, use the theorem prover to check whether all the
> >axioms in C are independent; i.e., none of them can be proved from
> >the remaining ones. If not, delete the redundant ones, but do so
> >one at a time to make sure that the deductive closure of the
> >remaining axioms is still equivalent to the original C.
> >
> >Now, it is possible that the theory is undecidable. But as I have
> >said before, that is also true of any theory constructed by hand.
> >But even at that level, it is easier to prove consistency (if it is
> >indeed provable) for multiple smaller theories than for one big theory.
> >
> >John Sowa
>
> Adam Pease
> Teknowledge
> (650) 424-0500 x571