Đồ ỏn tốt nghiệp đại học                                                      Đề                                                      Đề                                                                    Đề tài: Suy diễn tự động - Hệ thống suy diễn SLR

PHIẾU GIAO NHIỆM VỤ ĐỒ ÁN TỐT NGHIỆP

1. Thông tin về sinh viên

Họ và tờn sinh viờn: Nguyễn Thị Thỳy Mai

Điện thoại liờn lạc: 01682 957 498                            Email: nguyenttmai248@gmail. com

Lớp: Hệ thống thông tin B                                          Hệ đào tạo: Đại học chính quy

Đồ ỏn tốt nghiệp được thực hiện tại:Bộ môn Hệ thống thông tin - Khoa Công nghệ thông tin – Đại học Bách Khoa Hà Nội.

Thời gian làm ĐATN: Từ ngày    23/02/ 2009 đến  29/05/ 2009

2. Mục đích nội dung của ĐATN: Nghiờn cứu hai phương phỏp suy diễn tự động phổ biến là: phương phỏp SAT Solving với thủ tục DPLL và phương phỏp Theorem Proving với thủ tục hợp giải Resolution. Kết hợp hai phương pháp đó trong một phương pháp đúng đắn, đầy đủ và hiệu quả hơn là SLR-Satisfiability with Lazy Resolution. Cuối cùng là phần cài đặt phương pháp đó.

3. Cỏc nhiệm vụ cụ thể của ĐATN

v     Nghiờn cứu hai phương phỏp suy diễn tự động: phương phỏp SAT Solving với thủ tục DPLL và phương phỏp Theorem Proving với thủ tục hợp giải Resolution

v     Đọc code và chạy thử ví dụ của hệ thống DPLL

v     Kết hợp MiniSat + Spass

v     Tìm ví dụ và kiểm thử

v     So sánh với các hệ thống đã có (iProver, Darwin, Spass,…)

4. Lời cam đoan của sinh viờn:

Tôi –Nguyễn Thị Thỳy Mai - cam kết ĐATN là công trình nghiên cứu của bản thân tôi dưới sự hướng dẫn của TS. Trần Đức Khỏnh.

Các kết quả nêu trong ĐATN là trung thực, không phải là sao chép toàn văn của bất kỳ công trình nào khác.

5. Xỏc nhận của giỏo viờn hướng dẫn về mức độ hoàn thành của ĐATN và cho phộp bảo vệ:

Sinh viờn thực hiện: Nguyễn Thị Thỳy Mai – Khúa: K50 – Lớp: Hệ thống thông tin B              73