Re: [Core] Definition of strict safeness

> Safeness is a syntactic condition which guarantees finiteness and finite
> computability of the minimal model of a RIF Core ruleset. In the
> following, we define
> the different notions of safeness.

Please also explain what is meant with the concepts "finiteness" and
"minimal model" in the context of RIF Core.
Take into account that every RIF Core interpretation is necessarily
infinite, e.g., due to the guards.


Best, Jos

> 
> Option 1: no disjunction in Rule bodies
> =========================
> 
> A subformula of a RIF condition formula is called external sub-formula
> if it
> appears within an Externally defined term. A variable ?v  is called safe
> with respect
> to a RIF formula φ if it appears in at least one non-external atomic
> subformula
> ψ of φ
> such that ?v  is not in the  scope of an existential quantifier within
> ψ.
> A RIF condition formula φ is called strictly safe if all its
> variables are safe
> with respect to φ
> and for all its existential subformulas
> Exists ?V<sub>1</sub> ... ?V<sub>n</sub> ( &psi; ) each
> ?V<sub>1</sub>, ... , ?V<sub>n</sub> is safe with respect to &psi;
> A RIF rule &phi :- &psi; is called stricty safe if all its variables are
> safe with respect to
> &psi;.
> 
> Note: If we disallow nested existentials in Core than we can remove in
> this definition
> "such that v  is not in the scope of an existential quantifier within
> &psi;."
> as well as
> "and for all its existential subformulas Exists ?V<sub>1</sub> ...
> ?V<sub>n</sub> ( &psi; ) each ?V<sub>1</sub>, ... , ?V<sub>n</sub> is
> safe with respect to &psi;"
> 
> 
> Option 2: disjunction in Rule bodies over-cautions non-recursive definition
> ================================================
> 
> A subformula of a condition formula is called external subformula if it
> appears within an Externally defined term. A subformula of a condition
> formula
> is called disjunctive subformula if it appears within a Disjunction.
> A variable v  is called safe with respect to a RIF formula &phi; if it
> appears in
> at least one non-external, non-disjunctive atomic subformula of &phi;
> such that ?v  is not in the  scope of an existential quantifier within
> &psi;.
> 
> (the remainder of the definition is as for Option 1)
> 
> Option 3: disjunction in Rule bodies recursive definition:
> ====================================
> 
> A subformula of a condition formula is called external subformula if it
> appears within an Externally defined term.
> - A variable ?v  is called safe  with respect to a non-external, atomic
> RIF formula &phi; if
> it appears in &phi;.
> - A variable ?v is called safe with respect to a disjunction Or(
> &phi;<sub>1</sub> ... &phi;<sub>n</sub>) if ?v
> is safe with respect to each &phi;<sub>1</sub> ... &phi;<sub>n</sub>.
> - A variable ?v is called safe with respect to a conjunction Or(
> &phi;<sub>1</sub> ... &phi;<sub>n</sub>) if it
> is safe with respect to at least one of &phi;<sub>1</sub> ...
> &phi;<sub>n</sub>.
> - A variable is called safe with respect to an Existential  Exists
> ?V<sub>1</sub> ... ?V<sub>n</sub> ( &phi ) if
> (i) ?v != ?V<sub>1</sub> and ... and v != ?V<sub>n</sub>, and
> (ii) ?v is safe with respect to &phi, and
> (iii) all ?V<sub>1</sub> ... ?V<sub>n</sub> are safe with respect to &phi;
> 

-- 
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
One man that has a mind and knows it can
always beat ten men who haven't and don't.
  -- George Bernard Shaw