Belief Forgetting ของ Agent: ลืมตัวแปรแล้ว ข้อสรุปใดยังอยู่?

คำตอบสั้น: การลืมตัวแปรในตรรกศาสตร์ประพจน์คือการฉายสูตรไปยังภาษาที่เก็บไว้ โดยคงข้อสรุปทุกข้อที่เขียนด้วยตัวแปรที่เหลือไว้ได้ มันไม่ใช่การกำหนดค่าตัวแปรนั้นให้จริงหรือเท็จ และไม่ใช่การลบ clause ที่กล่าวถึงตัวแปรนั้นแบบตรงไปตรงมา บทความนี้ใช้สูตรที่ดัดแปลงสัญลักษณ์จาก Example 13 ของ Lang, Liberatore และ Marquis (2003): K=(¬p∨q)∧(p∨r) เมื่อลืม p จะได้ q∨r ทั้งนี้เป็นคุณสมบัติของตัวแทนเชิงตรรกะ ไม่ได้ยืนยันว่าระบบลบแถวข้อมูล บันทึก prompt หน่วยความจำภายนอก หรือพารามิเตอร์น้ำหนักของ LLM

Executive Answer — เก็บข้อสรุปในภาษาที่เหลือ

สมมติ Agent เก็บความสัมพันธ์ระหว่างตัวแปร p, q และ r ไว้ในสูตร แล้วผู้พัฒนาต้องการทำงานต่อโดยไม่ใช้ p อีก วิธีหนึ่งคือ propositional forgetting หรือการลืมตัวแปรในตรรกศาสตร์ประพจน์ เราเลือกชุดตัวแปรที่จะเก็บไว้ และคำนวณสูตรใหม่ซึ่งแทนโลกที่เป็นไปได้ทั้งหมดหลังฉายตัวแปรที่ลืมออก

จุดสำคัญคือสูตรใหม่ยังตอบคำถามใด ๆ ในภาษาที่เก็บไว้ได้ตรงกับต้นฉบับ หากคำถาม φ ไม่กล่าวถึง p แล้ว K อนุมาน φ ก็ต่อเมื่อผลจากการลืม p อนุมาน φ เช่นกัน ผลไม่จำเป็นต้องเก็บข้อความเดิมทุกชิ้น และไม่ได้เก็บตัวแปรที่ลืมไว้ในรูปเดิม แต่จะรักษาข้อสรุปทั้งหมดที่เกี่ยวกับภาษาส่วนที่เหลือ

สำหรับตัวอย่างนี้ สูตรต้นทางมีเงื่อนไขว่า ถ้า p เป็นจริง q ต้องจริง และถ้า p เป็นเท็จ r ต้องจริง เมื่อเราไม่สนใจว่า p เป็นค่าใด ก็ยังเหลือข้อสรุปว่า q หรือ r ต้องจริงอย่างน้อยหนึ่งตัว นี่คือ q∨r ความต่างกับการเลือกค่า p หรือทิ้ง clause จะเห็นได้จากการคำนวณในส่วนถัดไป

งานของ Lin และ Reiter ปี 1994 วางนิยามการลืมเชิงความหมายในบริบทของตรรกศาสตร์ และงานของ Lang, Liberatore และ Marquis ปี 2003 นิยามการลืมตัวแปรประพจน์ด้วยการแทนค่าจริงและเท็จแล้วเชื่อมผลด้วย OR พร้อมระบุคุณสมบัติการคงข้อสรุปในภาษาที่เหลือ งานเหล่านี้เป็นรากฐานทฤษฎี ไม่ใช่ผลประเมิน LLM หรือหลักฐานว่าระบบหน่วยความจำใดทำงานได้จริง (Lin & Reiter 1994; Lang et al. 2003)

Why It Matters — ตัดสินใจว่าจะเก็บภาษาใด

หน่วยความจำของ Agent มักถูกพูดถึงราวกับเป็นพื้นที่จัดเก็บข้อความเพียงอย่างเดียว แต่การทำให้ความรู้เป็นสูตรตรรกะเพิ่มอีกคำถามหนึ่ง: เมื่อเปลี่ยน vocabulary แล้ว ข้อสรุปใดจะยังใช้ได้? การลืมตัวแปรตอบคำถามนี้ในระดับแบบจำลองเชิงตรรกะ โดยกำหนดภาษาที่เหลือไว้อย่างชัดเจน

ตัวอย่างเช่น ระบบวางแผนสมมติอาจเข้ารหัสเงื่อนไขสถานะสามตัวไว้ แล้วงานย่อยต้องการเหตุผลเฉพาะตัวแปรปลายทางสองตัว การฉาย p ออกทำให้สูตรในภาษาของ q,r ใช้ต่อได้ โดยไม่บังคับให้ระบบเลือกว่าค่าเดิมของ p เป็นจริงหรือเท็จ ผล q∨r จึงบอกข้อจำกัดที่ยังตามมาจากสูตรต้นฉบับ ไม่ได้บอกว่า q หรือ r ตัวใดเกิดขึ้นจริง

แนวคิดนี้เชื่อมกับ belief revision และ minimal change แต่เป็นคนละกระบวนการ: revision ปรับฐานให้รับข้อมูลใหม่ ส่วน forgetting ฉายสูตรไปยัง vocabulary ที่กำหนด การสรุปความจำแบบย่อก็เป็นอีกชั้นหนึ่งซึ่งอาจทำข้อมูลหายหรือบิดเบือน โดยไม่รับประกันการคง entailment (memory consolidation แบบ lossy summary)

การรวมความเชื่อหลายฐาน เช่นในบทความ Belief Merging ก็ถามคนละเรื่อง: มันเลือกผลรวมจากหลายฐานภายใต้นโยบายและ integrity constraints ส่วน forgetting รับสูตรหนึ่งชุดแล้วเปลี่ยน vocabulary ที่ใช้แสดงผล

คำว่า “ลืม” จึงควรอ่านเป็นชื่อของ operator บนสูตร ไม่ใช่คำรับรองการลบข้อมูลจากระบบคอมพิวเตอร์ หาก Agent มีระบบเก็บประวัติ การลบหรือแก้ record ต้องจัดการเวลาและประวัติแยกต่างหาก ส่วนการวางแผนจาก belief state ก็ใช้ความสัมพันธ์ระหว่างโลกที่เป็นไปได้ แต่ไม่ได้ทำให้ผลของ logical forgetting กลายเป็นความจริงภายนอก

Scientific Foundations — นิยามและผลที่อ้างจากทฤษฎี

นิยามการฉายตัวแปร

ให้ K เป็นสูตรในภาษาประพจน์ และให้ V เป็นชุดตัวแปรที่เราต้องการลืม ภาษา K ที่ยังเก็บไว้คือ Var(K)\V สำหรับตัวแปรเดียว p นิยามตาม Lang et al. คือ (Definition 8, หน้า 410)

Forget(K,{p}) = K[p:=true] ∨ K[p:=false] = ∃p K

การแทน p ด้วยจริงและเท็จพิจารณาความเป็นไปได้ทั้งสองด้าน แล้วรวมด้วย OR: ผลเป็นจริงหากมีค่าอย่างน้อยหนึ่งค่าของ p ที่ทำให้สูตรต้นฉบับจริง สำหรับชุดตัวแปร V ทำซ้ำการกำจัดตามนิยาม ผลนี้เทียบเท่าการมี existential quantifier เหนือตัวแปรที่ลืมใน Boolean logic

สิ่งที่คงอยู่หลังลืม

REPORTED CLAIM — ผลที่ผู้เขียนรายงานในทฤษฎี: Lang et al. แสดงการเชื่อมโยงการลืมกับความเป็นอิสระของสูตรต่อตัวแปร และ Corollaries 5–7 ระบุการคงข้อสรุปที่ไม่กล่าวถึงตัวแปรที่ลืม รวมถึงลักษณะของผลว่าเป็นผลตามที่แรงที่สุดภายใต้ข้อกำหนด independence ตามนิยามของบทความ เราใช้คุณสมบัตินี้ในความหมายเชิง entailment เท่านั้น: ถ้า φ ไม่มีตัวแปรที่ลืม ความสัมพันธ์ K ⊨ φ และ Forget(K,V) ⊨ φ ตรงกัน (Definition 8, Example 13, Corollaries 5–7)

Lin และ Reiter (1994) ให้กรอบ semantic forgetting โดยพิจารณาการเปลี่ยนค่าของอะตอมที่ลืม ขณะที่ส่วนเกี่ยวกับกรณีประพจน์เชื่อมกับผลของการคงข้อสรุปที่ไม่เกี่ยวข้องกับตัวแปรนั้น การอ้างนี้ไม่ขยายไปถึงการลบประวัติหรือข้อมูลดิบในระบบจัดเก็บ

Worked Example — สูตรเต็ม ค่าที่กำหนด และผลฉาย

สูตร K=(¬p∨q)∧(p∨r) คือ สัญลักษณ์ที่เปลี่ยนชื่อจาก Example 13 ใน Lang et al. (2003), Example 13 (หน้า 410): ต้นฉบับใช้ (¬a∨b)∧(a∨c) และคำนวณผลการลืม a เป็น b∨c เราใช้ตัวอักษร p,q,r เพื่อให้เชื่อมกับตัวอย่าง Agent สมมติได้สะดวก สูตรและผลการคำนวณด้านล่างเป็นการวิเคราะห์ Boolean โดยตรงตามนิยาม ไม่ใช่ตัวอย่างใหม่ที่อ้างว่าเป็นของเรา

แทนค่า p=true ใน K จะได้ (false∨q)∧(true∨r), ซึ่งย่อได้เป็น q. แทนค่า p=false จะได้ (true∨q)∧(false∨r), ซึ่งย่อได้เป็น r. ดังนั้น

∃p K = K[p:=true]∨K[p:=false] = q∨r

q∨r ไม่บอกว่าทั้ง q และ r จริง และไม่ได้เลือกอย่างใดอย่างหนึ่ง แต่บอกว่าในทุกแบบจำลองที่สอดคล้องกับ K อย่างน้อยหนึ่งในสองตัวแปรนี้ต้องจริง นี่คือข้อสรุปของ K ที่เขียนได้โดยไม่ใช้ p

ระวังความต่างระหว่างสูตรเต็มกับผลฉายเมื่อเรา condition ค่า p ไว้ก่อน หากเพิ่มข้อเท็จจริง p สูตรเต็มคือ K∧p ≡ p∧q ไม่ใช่ q เพราะตัวแปร p ยังอยู่ในสูตรและยังถูกกำหนดว่าเป็นจริง ส่วนเมื่อเพิ่ม ¬p จะได้ K∧¬p ≡ ¬p∧r. หากฉายแต่ละสูตรที่ถูก condition ไปยังภาษา {q,r} จึงได้ q สำหรับกรณี p=true และ r สำหรับกรณี p=false. การแทนค่าในสูตรเดิมโดยตรงได้ q หรือ r เช่นเดียวกัน แต่เป็นการถามคนละคำถามกับ forgetting ซึ่งรวมสองกรณีเป็น q∨r

อีกวิธีที่อาจดูคล้ายคือเอา clause ที่มี p ออกทั้งหมด ในรูป CNF นี้มีสอง clause คือ (¬p∨q) และ (p∨r) การลบทิ้งทั้งคู่เหลือ ⊤ ซึ่งยอมรับทุกค่า q,r รวมถึง q=false,r=false จึงสูญเสียข้อสรุป q∨r. ANALYSIS: นี่เป็นการเปรียบเทียบกับกฎลบ clause แบบตรงไปตรงมาในสูตรตัวอย่างนี้ ไม่ใช่ทฤษฎีทั่วไปเกี่ยวกับวิธีลดรูป CNF ทุกชนิด

Technical Comparison — การเลือกค่าไม่เหมือนการฉาย

สำรวจ Projection — แบบจำลองเป็นเซต ไม่ใช่ข้อความที่ถูกซ่อน

SIMULATION: ห้องทดลองในเครื่องแสดงสูตรที่กำหนดไว้ล่วงหน้า K และ ⊥ เท่านั้น ไม่มี parser สำหรับรับสูตรทั่วไป และไม่มีการเชื่อมต่อฐานข้อมูลหรือหน่วยความจำของ Agent แบบจำลองของ K ในลำดับบิต p,q,r คือ 001, 011, 110, 111. เมื่อฉาย p ออก ค่า q,r ที่ได้คือ 01,10,11 จึงตรงกับสูตร q∨r

ความสัมพันธ์ระหว่างผลฉายกับโลกเต็มอาจแสดงด้วยการ lifting: เติมค่าตัวแปรที่ลืมได้ทุกแบบให้ assignment ที่เหลือ สำหรับ q,r ที่ได้จาก K การ lifting ของ {01,10,11} คือ {001,010,011,101,110,111} ซึ่งเป็นทุกโลกที่เข้ากันได้กับค่าคงเหลือ ไม่ใช่เฉพาะแบบจำลองต้นฉบับ เพราะ 010 และ 101 ไม่ทำให้ K จริง การแสดงนี้จึงไม่ใช่การกู้คืนโลกต้นทาง และผลฉายไม่ได้เก็บ provenance หรือ multiplicity ของแบบจำลองไว้

ผู้ทดลองเลือก subset ของ {p,q,r} ที่จะลืม ดูแบบจำลองที่เหลือ แล้ว Preview ก่อน Commit ได้ การเปลี่ยน fixture หรือ subset ทำให้ preview เดิมใช้ต่อไม่ได้ เพราะมันไม่ตรงกับ input รุ่นปัจจุบัน ปุ่ม Commit บันทึกผลจำลองทั้งชุดพร้อมเวอร์ชันในสถานะภายในของหน้า ไม่ได้เขียนลง external memory หรือบริการภายนอก

กรณีขอบช่วยแยก “ไม่มีคำตอบ” ออกจาก “ลืมทุกตัวแปร” หากลืมทุกตัวจากสูตรที่ยังมีแบบจำลอง ผลบน vocabulary ว่างมี assignment ว่าง ε หนึ่งค่า เขียนในตัวแทนของ Lab เป็น ['']. หากเริ่มจาก ⊥ ซึ่งเป็นสูตรขัดแย้งที่ถูกต้องตามตรรกะ จะไม่มีแบบจำลองและผลคือ []. การ Commit ผลว่างจากงาน ⊥ เป็นการบันทึกผล NO MODELS ของการทดลอง ไม่ใช่การปฏิเสธ input ว่าไม่ถูกต้อง และต่างจากสถานะเริ่มต้นที่ยังไม่เคย Commit

System Architecture — แยกสูตรจากระบบหน่วยความจำ

Conceptual Architecture / HYPOTHESIS: ตารางต่อไปนี้เป็นข้อเสนอสำหรับ Agent ที่เลือกแทนความรู้บางส่วนเป็นสูตรตรรกะ ไม่มีแหล่งที่อ้างว่าระบบทั้งหกโมดูลนี้ถูกนำไปใช้จริงกับ LLM หรือวัดผลแล้ว โครงสร้างมุ่งทำให้ขอบเขตของข้อมูลและความล้มเหลวมองเห็นได้

ขั้นตอนทั้งหมดข้างต้นเป็น HYPOTHESIS สำหรับออกแบบระบบ ไม่ใช่ข้อกำหนดจากนิยาม forgetting โดยตรง การเลือกว่าจะเก็บสูตรที่ฉายหรือคำนวณใหม่ทุกครั้งเป็นการตัดสินใจด้านระบบ การเก็บ audit trail ช่วยบอกว่าระบบสร้างผลใดจาก input รุ่นไหน แต่ไม่ได้รับรองว่า record ต้นทางถูกลบแล้ว

Operational Flow — ตรวจภาษาและเวอร์ชันก่อนเขียนผล

Conceptual Flow / HYPOTHESIS: ตัวอย่างย่อของ Agent ที่รับสูตรและ query; เป็นข้อเสนอด้านระบบ ไม่ใช่อัลกอริทึมที่อ้างว่าต้นฉบับติดตั้งไว้

Input: K (สูตร), X (vocabulary ต้นทาง), V (ชุดตัวแปรที่ลืม), φ (query), s (เวอร์ชัน snapshot)
Check: V ⊆ X; Var(φ) ⊆ X \\ V; s is current
Compute: P := ∃V K
Output: P, entailment result for φ, source/version references
Preview P; commit only after policy and freshness checks
On failure: return a typed error and keep prior records unchanged

เงื่อนไข query ป้องกันไม่ให้ผู้เรียกถามถึงตัวแปรที่ฉายออกไปแล้ว ส่วน version check ลดความเสี่ยงที่ระบบจะเขียน projection จาก snapshot เก่า การ Commit เข้า external memory เป็นการตัดสินใจแยกจากการคำนวณ และต้องมีสิทธิ์กับ audit ตามระบบจริง

เกมตรวจความเข้าใจ — เลือกการกระทำให้ตรงคำถาม

SIMULATION: เกมในหน้าเดียวกันสลับงานหกแบบ: ลืม p, ลืม q, ลืม r, ไม่ลืมตัวแปร, ลืมทุกตัวจาก K, และลืมทุกตัวจาก ⊥. ผู้เล่นต้องเลือกเซต assignment ที่ฉายได้ Preview และ Commit ผลที่ตรงโจทย์ ทุกงานคำนวณจาก fixture ที่ระบุ สำหรับงาน ⊥ เกมให้ผู้เล่นยืนยันชัดเจนว่าตั้งใจเลือกผล NO MODELS ก่อน Commit; ไม่มี benchmark หรือข้อมูลจริง

ในงานลืม p คำตอบคือ {01,10,11} บนลำดับ q,r. การเลือก {10,11} เท่านั้นเท่ากับ condition p=true แล้วฉาย ส่วนการเลือก assignment ทั้งสี่แบบเท่ากับผลจากการลบ clause ในตัวอย่างนี้ ทั้งสองทางเลือกจึงไม่ตรงกับคำสั่งลืม p. การเปลี่ยนงานหลัง Preview ต้องล้างผล preview เก่า และการเลือก [] สำหรับกรณี ⊥ นับเป็นผลที่ถูกต้อง ไม่ใช่ความล้มเหลวของเครื่อง

การเล่นจำลองนี้ตรวจได้เฉพาะชุดแบบจำลองจำกัดที่กำหนดไว้ในสัญญา Lab ซึ่งมีตัวแปรสามตัวและโลก Boolean แปดค่า ไม่ได้พิสูจน์ว่า engine ทั่วไปถูกต้องกับทุกสูตร ไม่ทดสอบความปลอดภัย ความเป็นส่วนตัว คุณภาพของข้อความธรรมชาติ หรือการลบข้อมูลจาก LLM

Applications — คำถามในภาษาที่เหลือ

REPORTED CLAIM: Corollary 7 ของ Lang et al. ระบุว่าข้อสรุปที่ไม่ใช้ตัวแปรที่ลืมยังคงตามมาจากผลฉาย ตัวอย่างการใช้เชิงตรรกะคือ query compilation: หาก query ใช้เฉพาะ {q,r}, สามารถตรวจ entailment กับ q∨r แทน K ได้โดยไม่เปลี่ยนคำตอบในภาษานั้น (Lang et al. 2003, Corollary 7).

HYPOTHESIS: Agent อาจเก็บ projection สำหรับงานย่อยและชี้กลับไปยังสูตรต้นทางด้วย version/provenance เพื่อให้อธิบายที่มาได้ ต้องประเมินความถูกต้องของการ formalize และต้นทุนของ query ก่อนใช้งานจริง; ทฤษฎีไม่ได้รับรองการเพิ่มความเร็วหรือความแม่นยำ

Limitations and Failure Modes — สูตรต้องถูกและแบบจำลองครบ

การฉายต้องรวมทุก assignment ที่มี extension ในภาษาต้นทาง หากแบบจำลองตกหล่น ผล entailment อาจเปลี่ยน สูตรที่มีตัวแปร n ตัวมีได้ถึง 2^n assignments; งานนี้ไม่มีการวัดต้นทุนหรือเปรียบเทียบ solver

กรณี ⊥ ไม่มีแบบจำลอง และ entailment แบบคลาสสิกจากมันเป็นจริงโดย vacuity สำหรับทุก query จึงต้องแสดงสถานะ NO MODELS แทนการนำผลไปใช้เป็นความจริงเชิงโลก ห้องทดลองรับเพียง fixture K และ ⊥; ไม่มี parser สำหรับ arbitrary formula. Formalization ผิดหรือ schema ที่เปลี่ยนความหมายทำให้ solver ที่ถูกต้องยังตอบโจทย์ผิดได้

Future Directions — แยกการตรวจ solver จากการตรวจ Agent

งานต่อไปอาจตรวจ entailment preservation บนชุดสูตรที่เผยแพร่ได้ พร้อมรายงานขนาดสูตร จำนวนตัวแปร และเวลา เพื่อให้ทำซ้ำได้ การประเมิน Agent ต้องแยกข้อผิดพลาดการแปลงภาษาเป็นสูตรออกจากข้อผิดพลาดของการฉาย และระบุ ground truth ก่อนทดลอง ส่วน privacy, record deletion และ model unlearning ต้องมีคำถามและหลักฐานคนละชุด; ไม่มีการทดลองเหล่านี้ในงานปัจจุบัน

Practical Takeaways — ตั้งขอบเขตให้ตรงก่อนเรียกว่า “ลืม”

ถ้าต้องการให้ความรู้เชิงตรรกะใช้ต่อได้หลังนำตัวแปรบางตัวออก ให้ระบุภาษาที่เก็บไว้และใช้ existential projection ตามนิยาม อย่าแทนการดำเนินการนี้ด้วยการตั้งค่าตัวแปรที่ลืมให้จริงหรือเท็จ เพราะนั่นเลือกกรณีเดียว และอย่าคิดว่าการลบ clause ที่กล่าวถึงตัวแปรจะคง entailment ไว้

หากต้องลบข้อมูลจริง ให้ระบุแหล่งจัดเก็บและขอบเขตที่ต้องลบ เช่น record, cache, log, prompt context หรือ external memory แล้วตรวจผลการลบตามกลไกของระบบนั้น การฉายสูตรไม่ได้เปลี่ยน storage layer เอง หากต้องการลดหรือกำจัดสิ่งที่โมเดลเรียนรู้จากข้อมูล ก็เป็นปัญหา machine unlearning ที่ต้องมีวิธีและหลักฐานของตัวเอง บทความนี้ไม่ได้ประเมินหรือให้คำรับรองนั้น

แยกชั้นข้อมูลสี่ส่วนนี้ออกจากสูตรตรรกะ:

FAQ

1. การลืมตัวแปรคือ existential quantifier ใช่หรือไม่?

ใช่ ในตรรกศาสตร์ประพจน์ การลืมตัวแปร p เขียนเป็น ∃p K ได้ และเทียบเท่ากับ K[p:=true]∨K[p:=false]. สำหรับชุดตัวแปรก็ทำซ้ำกับสมาชิกของชุดนั้น

2. ถ้าลืม p แล้ว q∨r แปลว่าทั้ง q และ r จริงหรือ?

ไม่ใช่ q∨r หมายถึงอย่างน้อยหนึ่งตัวต้องจริงในแบบจำลองของสูตร ไม่ระบุว่าตัวใดจริง และไม่ใช่ค่าความน่าจะเป็นหรือข้อสังเกตเกี่ยวกับโลกจริง

3. ทำไมไม่กำหนด p=true แล้วใช้ q?

นั่นคือ conditioning: สูตรเต็มคือ K∧p ≡ p∧q; เมื่อฉายสูตรที่ถูก condition ไปยัง {q,r} จึงได้ q. การลืม p ไม่เลือกค่าและรวมทั้งกรณีจริงกับเท็จเป็น q∨r

4. การลบ clause ที่มี p ใช้แทนได้ไหม?

ในตัวอย่างนี้ใช้แทนไม่ได้ เพราะการลบทั้งสอง clause เหลือ ⊤ ซึ่งยอมให้ q=false,r=false และไม่คงข้อสรุป q∨r. ประเด็นนี้เป็นการวิเคราะห์สูตรที่แสดง ไม่ใช่ข้อสรุปเกี่ยวกับทุกเทคนิคการจัดการ CNF

5. ผลการลืมรับรองว่า Agent ลบความทรงจำหรือข้อมูลส่วนตัวแล้วหรือไม่?

ไม่รับรอง มันคำนวณผลเชิงตรรกะของสูตรใหม่ การลบ record, log, retrieved context, external memory หรือพารามิเตอร์โมเดลต้องอาศัยกลไกและการตรวจสอบของชั้นจัดเก็บหรือกระบวนการเรียนรู้แยกต่างหาก

6. ผล [] กับ [''] ใน Lab ต่างกันอย่างไร?

[] หมายถึงไม่มี assignment ที่เป็นแบบจำลอง เช่น ⊥. [''] แทน assignment ว่างหนึ่งชุดเมื่อสูตรที่สอดคล้องกันถูกฉายจนไม่เหลือตัวแปร ทั้งสองเป็นผลจากงานที่ Commit แล้ว ส่วนสถานะเริ่มต้นยังไม่มีผลที่ Commit

References

1. Fangzhen Lin and Raymond Reiter. “Forget It!” AAAI Fall Symposium on Relevance, AAAI Technical Report FS-94-02 (1994), pp. 141–146. PDF ต้นฉบับจาก AAAI. อ่านทั้ง 6 หน้า โดยตรวจภาพหน้า 141–142 และ 146; ข้อความหลักที่ใช้: Definition 1, Propositions 2–3, Theorem 4 และผลสำหรับกรณีประพจน์ที่กล่าวถึงใน Theorem 11 หน้า 143–144. สถานะที่ระบุอย่างจำกัด: ผลงานประชุม AAAI Fall Symposium ปี 1994 ซึ่งเผยแพร่ใน technical report; ไม่กล่าวอ้างสถานะ peer review
2. Jérôme Lang, Paolo Liberatore, and Pierre Marquis. “Propositional Independence: Formula-Variable Independence and Forgetting.” *Journal of Artificial Intelligence Research* 18 (2003), 391–443. DOI: 10.1613/jair.1113. สำเนา PDF author-submitted บน arXiv; สารบัญ JAIR เล่ม 18. ตัว PDF ระบุส่ง 5/02 และตีพิมพ์ 5/03; สำเนาที่อ่านคือ arXiv v1 ส่ง 22 มิถุนายน 2011 ไม่อ้างว่า byte-identical กับไฟล์ผู้จัดพิมพ์ อ่านหน้า imprint, บทนำ หน้า 391–394, Definition 8 และ Example 13 หน้า 410, Corollaries 5–7 หน้า 410–411 และสรุป §6.2.1 หน้า 419. ภาพหน้าจริง 410–411 ยืนยันสมการและตัวอย่าง; ไม่ได้ replay proof

ขอบเขตการตรวจ: ไม่ได้ตรวจ repository, package, license หรือ implementation ปัจจุบัน จึงระบุ code availability เป็น UNKNOWN_NOT_INSPECTED. ไม่มี benchmark, reproduction, privacy evaluation หรือ weight-unlearning evaluation ในงานนี้ ผลของทฤษฎีใช้กับสูตรและ vocabulary ตามนิยามเท่านั้น