[Attempto] Should I allow for non-monotonic reasoning?

[Norbert E. Fuchs]

David

> Thank you Norbert for the attention to the error.
> I will test more when you fix RACE to your specifications.

OK.

> I request that you accept "is provably" in your syntax as it
> appears to be legal, even if it is superfluous, and following
> the Hiltz Principal of "Least Surprises" it would make ACE
> accepting of a varied input. Perhaps with a warning that the
> syntax is superfluous to help people writing ACE develop
> a sense of what is minimally necessary. 

We consider the status of ACE as stable, and will not add new language constructs. However, since ACE's parser APE is freely available, you are free to extend or modify the language in any way.

> Again, thank you for a great system. Perhaps you could 
> help those of us on the mailing list by presenting a small 
> portion of the code and explain how it is done ? This
> would allow us to develop more knowledge about ACE
> internal mechanisms.

A small portion of the code will not do considering the size of RACE. However, I plan to make the complete code of RACE public in due time.

Here is a summary of the main working of RACE:

RACE works with clauses of the form "Body -> Head" derived from the ACE axioms and theorems. Facts are represented as "true -> Head", negation as "Body -> fail". Clauses are executed bottom-up. If a Body can be proved from the data-base, then the respective Head is added to the data-base. All RACE clauses are range-restricted, i.e. all variables of Head  occur already in Body. As a consequence all proved Heads are variable-free.

Extending RACE by negation-as-failure does not immediately fit into this scheme since negation-as-failure is a meta concept, namely "check if a proof succeeds or fails and continue if it fails". Also, negation-as-failure – like in Prolog – does not instantiate variables. Now with negation-as-failure occurring in Body not all variables of Body are necessarily instantiated, and the derived and stored Head may contain uninstantiated variables which would allow for unwanted derivations. Eventually I found a way to artificially instantiate those variables, and everything seems to work fine so far.

Yet, on the basis of your examples I detected a bug. Negation-as-failure is processed separately from the rest which is subjected to some internal transformations. Unfortunately, I forgot to apply these transformations to the negation-as-failure part.

Best.

   --- nef