שיחה:מערכת הוכחה אינטראקטיבית

הערות

1. המשפט הראשון - אולי עדיף "בתורת הסיבוכיות, מערכת הוכחה אינטראקטיבית היא דיאלוג בין שתי קבוצות משתתפים שבמהלכו משכנעת קבוצת ה"מוכיחים" את קבוצת ה"מוודאים" בנכונותה של טענה חישובית מסויימת". "ייצוג מופשט של חישוב בתור דיאלוג"? אפשר בהמשך לומר שמערכות הוכחה משמשות לייצוג מופשט של חישובים.
2. "כמות המוכיחים" - "מספר המוכיחים".
3. בפסקה "NP כמערכת הוכחה" חסר ש- SAT היא NP complete.
4. "מתברר כי כוחה של מערכת ההוכחה הזו הוא גדול יחסית: ... IP זהה למחלקה PSPACE ... מחלקה גדולה יחסית": show, don't tell (בעיה שנמצאת ב-PSPACE ולא ב- ...).
5. Co-NP היא לא בדיוק "המחלקה המשלימה ל- NP" (ואם זו טרמינולוגיה מקובלת, אז היא מאד מבלבלת). עוזי ו. 11:41, 7 בנובמבר 2006 (IST)

תשובות:

1. יתוקן.
2. יתוקן. אתה האדם השני שאני שומע ממנו את התיקון הזה (בהקשרים שונים) בשבוע האחרון...
3. חסר, אבל אני לא חושב שרלוונטי כאן. SAT מובאת בתור דוגמה, ואיני בטוח שצריך להעמיס על הקורא בעוד מושג.
4. לא ברור מה אני אמור להראות, ואיך. ראשית, אולי PSPACE=P, אז להראות שפה שבודאות לא נמצאת ב-P אבל שייכת ל-PSPACE אי אפשר להראות (אלא אם אתה יכול, ואז אני חושב שיש לך מאמר לכתוב...). אפשר להראות את TQBF, שהיא PSPACE-שלמה, אבל לא ברור לי מה זה יגיד לקורא שלא כתוב כבר כעת. מה שכן ידוע הוא ש-PSPACE גדולה ממש מ-L (השפות שניתן לקבל ע"י מכונה דטרמיניסטית בזכרון לוגריתמי) וזה באמצעות משפט ההיררכייה לזיכרון - אבל זה די מסרבל לכתוב זאת כאן. לדעתי כדאי להשאיר את ה"להראות" לערך שעוסק ב-PSPACE.
5. אוי ואבוי. לא ברור לי מה לקחתי לפני שכתבתי את זה. יתוקן.

תודה רבה! גדי אלכסנדרוביץ' 13:51, 7 בנובמבר 2006 (IST)

הערה

בעקבות הפניה בדף ביקורת העמיתים- אני חסר ידע בנושא, וגם קריאה נוספת של פיסקת הפתיחה עדיין לא גורמת לי להבינה עד תומה. תוספת של הסבר אינטואטיווי יותר יכולה בהחלט להועיל, אני מאמין. שמעון נעים 21:42, 14 בדצמבר 2006 (IST)

תודה, אני אשמח לנסות ולשפר, אבל זה לא נושא שקל להציג אותו אינטואיטיבית. תוכל לנסות ולהצביע על נקודות שאתה מתקשה להבין? משפטים ספציפיים שאתה קורא ולא ברור לך מה רוצים ממך? הערות נקודתיות כאלו יכולות להיות מועילות מאוד. גדי אלכסנדרוביץ' 21:46, 14 בדצמבר 2006 (IST)

אנקדוטה על פיתוח מערכות הוכחה אינטראקטיביות

מסופר כי עבודתם של הצוות נדחתה מכנס STOCS/FOCS כשלוש פעמים, כנראה עקב החדשניות הרבה של הגדרות אלו, כך שלא ממש הבינו מה הוגדר, ולמה זה טוב. ההכרה הגיעה רק 10 שנים מאוחר יותר, עם הזכיה בפרס גדל. כיום כבר ברור שהגדרה זו הינה מעניינת מאד ומובילה לדיון בנושאי הוכחה באפס ידע. Gran - שיחה 09:02, 23 בפברואר 2010 (IST)

קישור שבור

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo
  • In Sharp-P on 2013-09-12 22:23:05, 403 Forbidden
  • In מחלקת סיבוכיות on 2013-09-13 03:28:20, 403 Forbidden
  • In סיבוכיות on 2013-09-13 04:32:53, 403 Forbidden
  • In Sharp-P on 2013-09-15 22:06:41, Socket Error: 'Connection timed out'
  • In מחלקת סיבוכיות on 2013-09-16 00:18:59, Socket Error: 'Connection timed out'
  • In Sharp-P on 2013-09-19 22:21:24, Socket Error: 'Connection timed out'
  • In Sharp-P on 2013-09-24 10:58:57, Socket Error: 'Connection timed out'
  • In מחלקת סיבוכיות on 2013-09-25 07:14:07, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:28:43, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:28, 25 בספטמבר 2013 (IDT)

קישור שבור 2

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:N#np
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:49:32, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:28:45, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:28, 25 בספטמבר 2013 (IDT)

קישור שבור 3

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:I#ip
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:49:46, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:28:48, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:29, 25 בספטמבר 2013 (IDT)

קישור שבור 4

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:P#pzk
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:49:32, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:29:08, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:29, 25 בספטמבר 2013 (IDT)

קישור שבור 5

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:S#szk
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:50:03, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:29:10, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:29, 25 בספטמבר 2013 (IDT)

קישור שבור 6

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:C#czk
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:50:03, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:29:28, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:29, 25 בספטמבר 2013 (IDT)

קישור שבור 7

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:M#mip
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:49:33, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:29:30, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:29, 25 בספטמבר 2013 (IDT)

קישור שבור 8

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:A#am
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:49:32, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:29:48, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:29, 25 בספטמבר 2013 (IDT)

קישור שבור 9

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:M#ma
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:50:03, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:29:50, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:30, 25 בספטמבר 2013 (IDT)

קישור שבור 10

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

• http://qwiki.stanford.edu/wiki/Complexity_Zoo:P#pcp
  • In מערכת הוכחה אינטראקטיבית on 2013-09-13 03:50:03, 403 Forbidden
  • In מערכת הוכחה אינטראקטיבית on 2013-09-16 00:31:30, Socket Error: 'Connection timed out'
  • In מערכת הוכחה אינטראקטיבית on 2013-09-25 08:29:58, Socket Error: 'Connection timed out'

--Matanyabot - שיחה 11:30, 25 בספטמבר 2013 (IDT)

אירית דינור

המשפט האחרון בערך מספר לנו שאירית דינור מצאה הוכחה חדשה למשפט ה-PCP. זה קצת מוזר לאור העובדה שאין מדובר בערך על המשפט ואפילו לא על PCP. אם כבר קודם על הערך לספר לנו מי הוכיחו את המשפט לראשונה, ולציין את כל אותם חוקרים רבים שהוכיחו את המשפט על גרסאותיו השונות, ולא רק את דינור. דניאל • תרמו ערך 16:44, 3 בנובמבר 2013 (IST)

בוודאי שצריך להיות ערך מלא על המשפט עצמו, ובו יספרו לנו גם על ההוכחה הראשונה למשפט. עם זאת, לא מדובר כאן בסתם הוכחה שניה למשפט מוכר: ההוכחה של דינור מספקת גישה ישירה אל לב המשפט, ויש לה השפעה רבה על התחום (דינור זכתה בגלל העבודה הזו בפרס ארדש). עוזי ו. - שיחה 18:19, 3 בנובמבר 2013 (IST)

אז הערך צריך לספר לנו על זה, כי כרגע המידע שנמסר סתום ומיותם. דניאל • תרמו ערך 18:37, 3 בנובמבר 2013 (IST)