Bezpečné formule DRK

• Df.: Bezpečná formule DRK, A, je formule DRK, která je definitní a syntakticky charakterizovatelná.

• 1. má eliminovaný 

• je-li v A obsažena disjunkce, pak je podformulí

• (x1,...,xs ) (x1,...,xs ),

• tj.  obsahují stejné volné proměnné,

• 3. je-li v A obsažena konjunkce (maximální), např.

•  r r1, pak každá volná proměnná ve

• je omezená, tj. platí pro ni alespoň jedna

• z podmínek:

  • proměnná je volná ve i  která není aritmetické porovnání a není negací,
  • existuje ix=a, kde a je konstanta,
  • existuje ix=y, kde y je omezená.