Warning:
This wiki has been archived and is now read-only.
Response to StH1
From RIF
From: Stijn Heymans <heymans@kr.tuwien.ac.at>
I read through the appendix on Herbrand Semantic Structures in the FLD, and am happy so see such a useful addition.
I have some questions/comments on a first reading though:
- "A Herbrand RIF-FLD universe, HU, is a set consisting of all the ground terms defined by RIF-FLD except the aggregate terms, external terms, and remote term references." Is this "set of ground terms" limited in some sense? In usual LP, when talking about the Herbrand universe one refers to the set of all constants appearing in some program P: is the "ground terms" referring to some a particular RIF-FLD document at hand (like "all ground terms appearing in document Tau")?
The Herbrand universe is defined with respect to all well-formed ground terms that that are constructible in a language of RIF-FLD. This has now been clarified.
- Should the definition of "ground instantiations" be with respect to a Herbrand universe? The domain D appears later in the definition of ground instance but is not a premise in itself of the definition?
Yes, fixed.
- In the definition of "ground instance", the term "replacement" might need further specification. What happens with quantifiers in formulas? (in usual LP, all variables are implicitly universally quantified, such that the definition for such formulas would be clear)
Thank you. This was a major oversight. It has been fixed now.
- The definition of minimality seems to have as an underlying intuition that a model I (a subset of the Herbrand base, as in LP) is minimal if for every other model I' is a superset of it ( I \subseteq I'). This is slightly different from what I am used to from Answer Set Programming where a model I is minimal if there is no other model I' such that I' \subseteq I. In other words, in the FLD definition a model I is minimal if it is a subset of all other models while in the latter definition it is minimal if there is no smaller one. Some short clarification would be helpful there..
This was another major bug in the definition. It has been fixed now.