Chulalongkorn University Theses and Dissertations (Chula ETD)

Generalization of certain types of clauses of the first-order predicate logic

Other Title (Parallel Title in Other Language of ETD)

การวางนัยทั่วไปของอนุประโยคตรรกศาสตร์เชิงเพรดิเคตอันดับที่ 1 บางชนิด

Year (A.D.)

1996

Document Type

Thesis

First Advisor

Boonserm Kijsirikul

Second Advisor

Mark E. Hall

Faculty/College

Graduate School (บัณฑิตวิทยาลัย)

Degree Name

Master of Science

Degree Level

Master's Degree

Degree Discipline

Computer Engineering

DOI

10.58837/CHULA.THE.1996.2395

Abstract

In the area of inductive learning, generalization is the main operation, and the usual definition of induction I based on logical implication, Plotkin’s well-known technique for computing least general generalizations of clauses under {u1D719}-subsumption sometimes sometimes produces results which are too general with respect to implication. Muggleton has shown that this problem only occurs in one type of gencralization of recursive clauses, called an indirect root. Idestam-Almguist presented a technique, called recursive anti-unification, to compute indirect roots of clauses. However there exist cases for which recursive anti-unification does not work, cases where at least one of the clauses contains a structure called a cross connection. In this research, we develop a technique for computing indirect roots of Horn clauses. We firat introduce a relation equivalent to implication, called {u1D719}-proof, which is syntactically defined, using resolution and {u1D719}-subsumption. This leads us to an algorithm, the J-algorithm, for computing indirect roots of clauses. Because the J-algorithm makes no assumptions about the structure of its input clause, it can compute roots of clauses containing cross connections. We also prove that the output from the algorithm is a generalization under implication of the input.

Other Abstract (Other language abstract of ETD)

การวางนัยทั่วไปมีความสำคัญอย่างยิ่งในศาสตร์ทางการเรียนรู้โดยอุปนัย หรืออาจกล่าวได้ว่าบทนิยามทั่วไปของการอุปนัยมีพื้นฐานมาจากการแจงเหตุสู่ผลเชิงตรรกะ ซึ่งการเรียนรู้โดยอุปนัยส่วนใหญ่ในปัจจุบันนี้ นิยมใช้การแสดงอนุประโยคด้วยวิธีการวางนัยทั่วไปภายใต้เซตาสับซัมชัน ซึ่งคิดค้นโดย Plotkin เนื่องจากเทคนิคนี้เป็นเทคนิคที่มีประสิทธิภาพสูง และเป็นที่รู้จักกันดีสำหรับผู้ที่ศึกษาทางด้านนี้ อย่างไรก็ตาม Muggleton ได้แสดงให้เห็นว่าวิธีของ Plotkin นี้มีความสามารถคำนวณหาการวางนัยทั่วไปเพียงกว้าง ๆ เท่านั้น โดยเฉพาะเมื่อใช้กับอนุประโยคชนิดอินไดเรกรูต ซึ่งเป็นอนุประโยคแบบรีเคอลีฟชนิดหนึ่ง ต่อมา Idestam-Almquist ได้เสนอเทคนิคที่เรียกว่าแอนตียูนิฟิเคชันแบบรีเคอลีฟ ที่สามารถใช้กับอนุประโยคชนิดอินไดเรกรูตได้ แต่อย่างไรก็ตามยังมีอนุประโยคแบบครอสคอนเนกชันที่มีคุณสมบัติเป้นอินไดเรกรูต ซึ่งไม่สามารถหาได้โดยวิธีของ Idestam-Almquist ดังนั้นวิธีดังกล่าวจึงไม่สมบูรณ์สำหรับอนุประโยคแบบครอสคอนเนกชัน ในงานวิจัยนี้ ผู้วิจัยได้พัฒนาเทคนิคสำหรับคำนวณหาการวางนัยทั่วไปของอนุประโยคชนิดอินไดเรกรูต เฉพาะอนุประโยคแบบฮอร์นเท่านั้น ผู้วิจัยได้กำหนดการพิสูจน์แบบเซต้า ซึ่งเป็นความสัมพันธ์กับการแจงเหตุสู่ผล โดยใช้นิยามของรีโซลูชันและเชตาสับซัมชัน นอกจากนี้ผู้วิจัยยังได้ทำการออกแบบขั้นตอนวิธีแบบเจขึ้น เพื่อใช้คำนวณหาการวางนัยทั่วไปของอนุประโยคชนิดอินไดเรกรูตแบบครอสคอนเนกชันได้ และผลที่ได้คืออนุประโยคที่มีคุณสมบัติเป็นการวางนัยทั่วไปภายใต้การแจงเหตุสู่ผล

Link to Full Text

Share

COinS