אינדוקציה שלמה ואינדוקציה רגילה

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

פותרים את SAT – אלגוריתם CDCL

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

פותרים את SAT – אלגוריתם DPLL

הגענו סוף סוף לדבר על האופן שבו פותרים את בעיית SAT במקרה הכללי. יש לנו פסוק CNF $latex \varphi$ ואין לו בהכרח צורה "נחמדה" כמו בבעיות 2SAT או HORNSAT שראינו בפוסט הקודם – מה עושים? ראשית כל ההסתייגות הבלתי נמנעת … להמשיך לקרוא

פותרים את SAT: המקרים של HORNSAT ו-2SAT

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

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

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

מה זו בעיית SAT ולמה חשוב לפתור אותה?

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

על P=NP מעל חבורות אבליות – סוף דבר

בשני הפוסטים האחרונים אני מכין את הקרקע לקראת הוכחה ש-$latex \mbox{P}\ne\mbox{NP}$ במודלים חישוביים שהם מעל חבורות אבליות אינסופיות. בפוסט הראשון הצגתי את הרעיון שמאחורי מודל חישובי שכזה והצגתי הוכחה לכך שעבור המקרה הקונקרטי של $latex G=\mathbb{Z}$ אנחנו אכן מקבלים ש-$latex … להמשיך לקרוא

על על-מסננים ועל-מכפלות

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

על P=NP מעל חבורות אבליות – מבוא שלם

בואו נוכיח ש-$latex \mbox{P}\ne\mbox{NP}$. אה… מה? תיארתי בעבר בבלוג את בעיית $latex \mbox{P=NP}$ בתור הבעיה הפתוחה המרכזית במדעי המחשב ולא הרבה השתנה מאז – עדיין אין לנו הוכחה ש-$latex \mbox{P}\ne\mbox{NP}$ למרות שרוב מדעני המחשב חושבים שזה המצב. אז מן הסתם … להמשיך לקרוא

מכסחי הכמתים

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

לוגיקה מסדר ראשון – כמה תוצאות של משפט השלמות

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

משפט השלמות של גדל, ההוכחה (חלק ב')

אנו ממשיכים בהוכחת משפט השלמות של גדל. כזכור, בפוסט הקודם הוכחנו שאם $latex \Phi$ היא תורה עקבית מקסימלית מעל מילון $latex \tau$ שבנוסף לכך קיימת עבורה קבוצת עדים $latex C$, אז קיים ל-$latex \Phi$ מודל. זה מספיק כדי לסיים את … להמשיך לקרוא

משפט השלמות של גדל, ההוכחה (חלק א')

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

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

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

פרדוקס בוחן הפתע

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

הבעיה העשירית של הילברט – פונקציות דיופנטיות וחיות אחרות (רקורסיביות)

אנו ממשיכים בדרך שלנו אל ההוכחה שלא קיים אלגוריתם שפותר את הבעיה העשירית של הילברט. אני מניח שקראתם את פוסט המבוא ולכן קופץ ישר לעניינים הפעם. המושג המרכזי בפוסט הקודם היה קבוצה דיופנטית. זוהי קבוצה $latex S=\left\{ \left(a_{1},\dots,a_{n}\right)\right\} $ של … להמשיך לקרוא

לוגיקה מסדר ראשון

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

תחשיב הפסוקים – משפט הקומפקטיות ואיך משפט השלמות דומה למשפט טיכונוף

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

משפט השלמות לתחשיב הפסוקים

בפוסט הקודם הצגתי מערכת הוכחה (חלקית, עוד לא גמרנו) לתחשיב הפסוקים והוכחתי שהיא מקיימת את משפט הדדוקציה: אם $latex \Phi\cup\left\{ \alpha\right\} \vdash\beta$ אז $latex \Phi\vdash\alpha\to\beta$. הפעם אני רוצה להמשיך לבנות את מערכת ההוכחה הזו ולהראות שהיא מקיימת את התכונה שלשמה … להמשיך לקרוא

תחשיב הפסוקים – על נביעה לוגית והוכחות

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