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

[Douglas Miles]

What language is RACE in?

/me hopes its prolog!

On Wed, Aug 12, 2015 at 12:55 AM, Norbert E. Fuchs <fuchs at ifi.uzh.ch> wrote:

>
> 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
>
>
> _______________________________________________
> attempto mailing list
> attempto at lists.ifi.uzh.ch
> https://lists.ifi.uzh.ch/listinfo/attempto
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20150812/2aa54c82/attachment.html>