מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

6.6.2. פעולות על קבוצות

פעולות סטנדרטיות:

איחוד, חיתוך, השלמה, השוואה וכדו'.

פעולות נוספות:

$plot:$\exists {x_i},f\left( {{x_1},...,{x_n}} \right)$$ - מחשבים האם יש הצבה של $plot:${x_i}$$ הנותנת לפונקציה ערך אמת.
$plot:$\forall {x_i},f\left( {{x_1},...,{x_n}} \right)$$ - מחשבים האם כל הצבה של $plot:${x_i}$$ נותנת לפונקציה ערך אמת.

נשים לב כי מתקיים:

$plot:$\exists {x_i},f\left( {{x_1},...,{x_n}} \right) = f{\left( {{x_1},...,{x_n}} \right)_{{x_i} = 1}} \vee f{\left( {{x_1},...,{x_n}} \right)_{{x_i} = 0}}$$

$plot:$\forall {x_i},f\left( {{x_1},...,{x_n}} \right) = f{\left( {{x_1},...,{x_n}} \right)_{{x_i} = 1}} \wedge f{\left( {{x_1},...,{x_n}} \right)_{{x_i} = 0}}$$

כלומר, הפעולות הנוספות לא נותנות לנו עוד כוח ביטוי. הפעולות הנוספות נותנות לנו סימונים נוחים לכתוב פעולות כשנזדקק להן.

דגש נוספת לגבי פעולות אלו הינו שאלו פעולות יקרות יחסית לאיחוד, חיתוך ושאר הפעולות הסטנדרטיות. למשל, חישוב של $plot:$\exists {x_1},{x_2},..,{x_n}:f\left( {{x_1},...,{x_n}} \right)$$ חסום על ידי $plot:${2^n}$$ פעולות. (נגיע לחסם זה על ידי שנשים לב שעבור כל $plot:${x_i}$$ מבצעים 2 פעולות, ומבצעים מכפלה plot:$n$ פעמים עבור כל האפשרויות ל- $plot:${x_i}$$ השונים.