The status of Axiomatic Formulas

[miquelramirez]

Axiomatic formulae have been disabled in this iteration. Quoting the comment in the code:

The distinction between whether a formula is axiomatic, external, etc. should probably be done elsewhere, not here (possibly at the evaluation level)

Like the implication, "axiomatic" formulas of the form

\phi \iff \varphi

can be rewritten, compiling the equivalence operator away. This form of syntactic sugar is somewhat controversial, because of the tendency in the planning literature of conflating the semantics of the constraint (phi and varphi need to be simultaneously satisfiable in all worlds) with the vagaries of the syntactic restrictions enforced by planners so as to make transition functions, heuristics and what not tractable/simple/easy.

My idea with axiomatic formulas in Tarski is that they are what they are: the bi conditional. How they're compiled, handled or what restrictions are forced on other elements of the language, such as action effects, is something for the back ends to handle as it suits them best.

[gfrances]

Yes, but (just to add to what you say) axioms have certain additional syntactic constraint, right, i.e. cannot be arbitrary formulas, but follow a logic-programming-rule approach: the head of the axiom needs to be an atom, the body could in principle be any arbitrary formula. More syntactic restrictions: the top predicate symbol in the head needs to be a "secondary" symbol, i.e. cannot appear in the head of any action effect; cannot of course be any fixed builtin symbol. Any other? Will check Thiebaux's "In defense of ..." later

[gfrances]

OTOH, what I meant with the comment you quote is: do we really need to make a distinction in the formula hierarchy for axioms?? Conceptually, an axiom IS a LP rule that binds the meaning of certain symbols in any interpretation of the language that we consider valid. i.e. it's clearly a semantic, not syntactic construct. At the syntactic level, say, I might have an atom clear(b). Whether I impose some axiomatic definition on clear or not (i.e. define it as an axiom or define it as a fluent), is largely irrelevant at the syntactic level - it is just an atom: predicate symbol followed by some arguments which are terms. Full stop. True enough, there's some additional syntactic restrictions as I said on the comment above: if clear is an axiom, the atom cannot appear on the head of an action effect. But this is a syntactic restriction above the level of the multi-sorted first-order language, i.e., it pertains to the FSTRIPS level, and, as such, we should not pollute our FOL design with considerations about this. The "language layer" in tarski should be as pure a FOL as possible; and, in this case, I think that taking these considerations out of the FOL layer does really not complicate the design too much - we will just need to enforce that simple syntactic constraint elsewhere, possibly when constructing the action, etc. What do you think, miquel?

[miquelramirez]

It is syntactic sugar. Sugar is sometimes good, and sometimes bad, especially when taken in great quantities.

First of all, I am not proposing to make room for axioms to force into anyone to grab a handful of salt and scrub it in their eyes. Which is pretty much what the extremely limiting specification of axioms for planning proposed, nearly 15 years ago. Indeed, Horn Clauses have nice computational properties, and if whatever constraints are needed by the modeller fit that fragment of FOL, he/she can get a rock and hit themselves in the teeth to celebrate how fortunate they are. The history behind that paper is that Hoffman insisted that whatever was proposed should be "friendly" to the FF relaxed plan heuristic so...

With that in mind - that axioms can be more than Horn Clauses - I still think that allowing for the front end to represent them in a distinctive way to help back ends makes sense and is an intelligent part of the design of FS that we can transfer to Tarski without feeling too bad.

Certainly, we could compile them automatically to CNF - as we do with the implication - but that dissolves the information contained by the original connective, and we force the backend to figure it from first principles. Too many papers like that have been written already, I think.

[gfrances]

Interesting intra-history! I'm certainly open to rethink that limitation, no need to say! So you're suggesting to go for full-FOL (that sounds nice) version of axioms, where an axiom is... well, an axiom :-) i.e. a sentence that must hold in any valid interpretation of the world. In other words, what we elsewhere called state constraints, right? I'm not a big fan of the choice of word axiom, as it is too connoted with so many non-equivalent meanings... but is that precisely what you have in mind?

Related point (assuming the above is what you have in mind): how do I use this to define e.g. clear axiomatically?

[miquelramirez]

Interesting intra-history! I'm certainly open to rethink that limitation, no need to say! So you're suggesting to go for full-FOL (that sounds nice) version of axioms, where an axiom is... well, an axiom :-)

Yep.

In other words, what we elsewhere called state constraints, right? I'm not a big fan of the choice of word axiom, as it is too connoted with so many non-equivalent meanings... but is that precisely what you have in mind?

Regarding nomenclature: here we're following the current implementation in FS, where state constraints and axioms are formulas follow similar syntax rules. The difference is that for state constraints the "head" is True, for axioms we allow the "head" to be an atom.

I think that it would be for the better to refer to them as "trajectory constraints" or "state constraints" or "global constraints"... or perhaps just "constraints" :) as these formulae specify properties that the transition function needs to comply with. In fact, my vision is to get events and processes into this category too, the difference being that the formula is a temporal one (as it refers "next states").

[miquelramirez]

Related point (assuming the above is what you have in mind): how do I use this to define e.g. clear axiomatically?

I need to think about it :)

[gfrances]

for state constraints the "head" is True

Not sure I understand this? You mean that a state constraint is like a LP rule where the body is the negated constraint and the head is false? i.e. thereby preventing the negation of the state constraint to be sastisfied in any state. My point is that thinking about state constraints as LP rules perhaps unnecessarily complicates things - thinking about the as "arbitrary formulas that must hold in any state" seems clearer to me?

[miquelramirez]

thinking about the as "arbitrary formulas that must hold in any state" seems clearer to me?

Yes, that's the way they need to be defined. I was trying to reconstruct the attempt at unification (without pissing off the planning literature) which we use to rationalise the current implementation in FS.