CALM issue -- classical negation allowed in head of a definition?

[zhangyuanlin]

CALM complains about this definition

-accessible_to(X, Y) if -is_accessible(X).

We assume CALM is right?

Definition of "definition" from ALM paper:

The definition of a defined function p is an expression of the form
     p(t1) if cond1
        ... 
     p(tk) if condk
where t's are sequences of terms, and cond1 , . . . , condk are collections
of literals. Moreover, if p is a static then cond1, . . . , condk can not 
contain fluent literals. Statements of the definition will be often 
referred to as its clauses. The statement says that, for every Y, 
p(Y) is true in a state σ iff there is 1≤m≤k such that statements 
condm and tm =Y are true in σ.

[Topology]

Definitions are boolean functions that have the closed world assumption added. If they are not defined to be positive, they will be negative by default. The usage of fluent function definitions in my mind is basically as "indicators". You set flags to become true when certain conditions are met, and false otherwise. They do not preserve their truth state through law of inertia, like boolean functions that are basic fluents.

what is the scenario being modeled?

[zhangyuanlin]

Anu,

Can you send the program to Edward?

Cheers, Yuanlin

On Sep 1, 2018, at 11:18 AM, Edward Wertz notifications@github.com<mailto:notifications@github.com> wrote:

Definitions are boolean functions that have the closed world assumption added. If they are not defined to be positive, they will be negative by default. The usage of fluent function definitions in my mind is basically as "indicators". You set flags to become true when certain conditions are met, and false otherwise. They do not preserve their truth state through law of inertia, like boolean functions that are basic fluents.

what is the scenario being modeled?

—

[Topology]

Aside: The reason I break up the axioms into labelled groups is because there is an overlap on the syntax of state constraints and function definitions. A basic boolean function can occur in the head of state constraints, defined boolean functions occur in the head of function definitions. The grammar is ambiguous here. (parser misfiring between the non-terminal for state constraints and function definitions). I wanted a strong syntactic marker to distinguish the two kinds of axioms and avoid the ambiguity. Another bonus is enhanced readability and reasoning for humans. With everything intermingled it becomes hard to recall what type of axiom we are looking at. It also promotes modularity. If any of the axiom sections are getting too large, it is a good indicator that the module should be split into 2.

[zhangyuanlin]

(Ed's email 9/1) I've commented there. Given that function definitions have the closed world assumption (page 12 of the ALM paper), is there a need to force them to be negative instead of only defining when they are positive?

I think it is clear now. No classical negation should be allowed in the head of a definition, as in ALM paper.