Re: SUO: a silly question about the new modular architecture
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