רזולוציה – איך אפשר להוכיח שאי אפשר?

בפוסט הקודם תיארתי את בעיית SAT וסיימתי בכך שהבטחתי להסביר איך אפשר להשתכנע בכך שפסוק CNF אינו ספיק, מבלי שיהיה צורך לבדוק את כל ההשמות האפשריות עבורו. בפוסט הזה אציג את השיטה הנפוצה ביותר לשימוש כדי להוכיח זאת – רזולוציה. … להמשיך לקרוא

מערכת הוכחה ללוגיקה מסדר ראשון

סדרת הפוסטים שלי על לוגיקה הגיעה עד לתיאור של הסינטקס והסמנטיקה של לוגיקה מסדר ראשון ושם עצרתי, כי השלב הבא, שעליו אני רוצה לדבר עכשיו, הוא לא פשוט. בתחשיב הפסוקים, שהצגתי בתור "חימום" ללוגיקה מסדר ראשון, היעד שלנו היה הצגת … להמשיך לקרוא

אז מה זה IP=PSPACE?

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

משפט ה-PCP או: איך למדתי להפסיק לדאוג ולאהוב הוכחות הניתנות לבדיקה הסתברותית

אחד מהנושאים הלוהטים ביותר במדעי המחשב המודרניים הוא משפט ה-PCP, הרחבותיו והשלכותיו. אלא שכל הקשור ל-PCP עשוי להישמע מוזר מאוד כששומעים לראשונה מה ראשי התיבות הללו מסמלים: Probabilistically Checkable Proofs, הוכחות הניתנות לבדיקה הסתברותית. מה זה בכלל, ואיך אפשר לזהם … להמשיך לקרוא