Logic mô tả

Lôgíc mô tả (tiếng Anh: "Description logics", viết tắt "DL") là một họ các ngôn ngữ biểu diễn tri thức có thể sử dụng để biểu diễn tri thức thuật ngữ của một miền ứng dụng theo một cách có cấu trúc và được hiểu rõ một cách hình thức. Mặt khác, cái tên "lôgíc mô tả" có ý nói đến các mô tả về khái niệm được dùng để mô tả một miền và ngữ nghĩa dựa lôgic ("logic-based semantics") mà có thể thu được từ việc dịch từ lôgic mệnh đề bậc nhất.
Lôgic mô tả được thiết kế như là một mở rộng của khung ngữ nghĩa ("semantic frame") và lưới ngữ nghĩa ("semantic network"), hai loại này đã không được trang bị một ngữ nghĩa dựa lôgic hình thức.
Lôgic mô tả được đặt cái tên hiện dùng từ năm 1980. Trước đó, nó đã được gọi là các "hệ thống thuật ngữ" ("terminological system"), và tiếp đó là các "ngôn ngữ khái niệm" ("concept language"). Ngày nay, lôgic mô tả đã trở thành một nền móng của Web Ngữ nghĩa ("Semantic Web") do việc sử dụng nó trong thiết kế các bản thể ("ontology").
Hệ thống dựa lôgic mô tả đầu tiên là KL-ONE (do Brachman và Schmolze xây dựng năm 1985).
Một số hệ thống lôgic mô tả khác xuất hiện sau đó là LOOM (1987), BACK (1988), KRIS (1991), CLASSIC (1991), FaCT (1998) và gần đây là RACER (2001), CEL (2005), và KAON 2 (2005).
Ý tưởng cho sự phát triển của Tầng Suy luận Bản thể ("Ontology Inference Layer - OIL") đã xuất phát từ lôgic mô tả.
Cú pháp.
Cú pháp của lôgic mô tả bao gồm 
Trong lôgic mô tả, các tên khái niệm được xem là các khái niệm nguyên tử, các tên vai trò được coi là các vai trò nguyên tử. Nhìn chung, một khái niệm đại diện cho tập các cá thể thuộc về nó, và một vai trò đại diện cho một quan hệ giữa các khái niệm.
Cú pháp của một thành viên trong gia đình lôgic mô tả được đặc trưng bởi định nghĩa đệ quy của nó, các định nghĩa đệ quy này định nghĩa các tạo tử có thể được dùng để tạo các thuật ngữ khái niệm.
Một số tạo tử thông dụng bao gồm các tạo 
tử lôgic trong logic bậc nhất như "phép giao" ("intersection") hay "tuyển" ("conjunction") của các khái niệm, "phép hợp" ("union") hay "hội" ("disjunction") của các khái niệm, "phép phủ định" ("negation") hay "lấy phần bù" ("complement") của các khái niệm, "hạn chế giá trị" (hạn chế "với mọi" - "universal restriction"), hạn chế "tồn tại" ("existential resctriction"), v.v.. Các tạo tử khác có thể còn bao gồm các hạn chế đối với các vai trò thường thấy trong các quan hệ nhị phân, ví dụ, tính đảo ("inverse"), tính bắc cầu ("transitivity"), chức năng ("functionality"), v.v.. Đặc biệt đối với phép giao và phép hợp, lôgic mô tả sử dụng các ký hiệu formula_1 và formula_2 để phân biệt chúng với ∧ và ∨ trong lôgic bậc nhất.
Dưới đây là một ví dụ về định nghĩa cú pháp của lôgic mô tả AL.
Ví dụ, formula_7 là một khái niệm-AL, nhưng formula_8 không phải. Còn nữa, formula_9 là một khái niệm-AL, nhưng formula_10 thì không phải.
Ngữ nghĩa.
Ngữ nghĩa của lôgic mô tả được định nghĩa bằng cách giải nghĩa các khái niệm như là các tập hợp gồm các cá thể, và các vai trò như là các tập gồm các cặp cá thể. Các cá thể đó thường được cho là thuộc một miền xác định cho trước. Sau đó, ngữ nghĩa của các khái niệm và vai trò không nguyên tử được định nghĩa theo các khái niệm và vai trò nguyên tử. Điều này được thực hiện bằng một định nghĩa đệ quy tương tự như trong cú pháp.
Ví dụ, cho trước miền xác định là một tập hợp. Trước hết, một cách giải nghĩa các khái niệm-AL được định nghĩa qua các khái niệm và vai trò nguyên tử như sau:
Tiếp theo, cách giải nghĩa này được mở rộng tới khái niệm và vai trò không nguyên tử, bằng cách sử dụng các tạo tử. Việc này được thực hiện như sau.
Do đó, theo cách giải nghĩa các khái niệm và vai trò như trên, nếu P được giải nghĩa là tập tất cả mọi người và F được giải nghĩa là tập tất cả phụ nữ, thì tập tất cả những người không phải phụ nữ có thể được biểu diễn bằng khái niệm 
Mô hình hóa bằng lôgic mô tả.
Trong các lôgic mô tả, có sự phân biệt giữa cái gọi là TBox (hộp thuật ngữ) và ABox (hộp khẳng định). Nói chung, TBox chứa các câu mô tả các cây phả hệ của các khái niệm (nghĩa là quan hệ giữa các khái niệm) trong khi ABox chứa các câu có nội dung xác định mỗi cá thể thuộc về vị trí nào trên cây phả hệ (nghĩa là quan hệ giữa các cá thể và các khái niệm). Ví dụ, khẳng định:
(1) "Mỗi nhân viên là một người
thuộc về TBox, còn khẳng định:
(2) "Hà là một nhân viên
thuộc về ABox. Lưu ý rằng sự phân biệt TBox/ABox trong lôgic mô tả không có ý nghĩa như vậy trong logic bậc nhất (hầu hết các lôgic mô tả đều có thể xếp vào loại lôgic này). Hai "loại" câu này được đối xử như nhau. Khi dịch sang lôgic bậc nhất, một tiên đề xếp loại như (1) chỉ là một hạn chế có điều kiện cho các mệnh đề đơn (khái niệm) mà trong đó chỉ có các biến. Rõ ràng, một câu thuộc dạng này không được ưu tiên đặc biệt so với các câu chỉ chứa các hằng như (2).
Vậy tai sao lại phân biệt như thế? Lý do chính là vì sự tách biệt đó có thể có ích khi mô tả và hệ thống hóa các quy trình-quyết định cho các lôgic mô tả khác nhau. Ví dụ, một bộ lập luận có thể xử lý TBox và ABox riêng rẽ, phần vì một số bài toán suy luận quan trọng được gắn chặt với chỉ một trong hai hộp (bài toán 'phân loại' liên quan đến TBox, bài toán 'kiểm tra thực thể' ("instant checking") gắn với ABox). Một ví dụ khác là độ phức tạp của TBox có thể ảnh hưởng lớn tới hiện quả làm việc của một quy trình-quyết định cho trước của một hệ lôgic mô tả nào đó, mà không phụ thuộc vào ABox. Do đó, đây là một cách hữu dụng để có thể nói về phần cụ thể đó của cơ sở tri thức.
Lý do phụ là sự phân biệt đó là có nghĩa nếu nhìn từ góc độ người mô hình hóa cơ sở tri thức. Đối với họ, việc phân biệt giữa quan niệm của ta về các thuật ngữ/khái niệm trong thế giới (các tiên đề phân loại trong TBox) và các thể hiện cụ thể của các thuật ngữ/khái niệm đó (các khẳng định thực thể trong ABox.)
Các bộ lập luận dành cho lôgic mô tả.
Có một số bộ lập luận ("reasoner") để làm việc với OWL và lôgic mô tả. Dưới đây là một số chương trình thông dụng nhất:
Các công cụ khác có liên quan dành cho Lôgic mô tả: