Tôi muốn chính thức hóa một số kiến thức và thực hiện các truy vấn trong những gì có thể được gọi là khai báo đầy đủ Horn logic (hoặc Prolog). Bất cứ ai có thể cung cấp một số hướng dẫn về cách thực hiện nó? Tôi tóm tắt ngắn gọn mô tả tốt từ liên kết ở trên:Làm thế nào để thực hiện logic Horn đầy đủ khai báo?
Ngôn ngữ chính thức là (cốt lõi) Prolog: một "chương trình" là một bộ quy tắc và sự kiện như trong Prolog (bao gồm các hàm và biến và về cơ bản) chỉ chứa các biến vị ngữ do người dùng xác định).
Ngược lại với Prolog, tuy nhiên, tôi đang tìm cách triển khai âm thanh và hoàn chỉnh liên quan đến ngữ nghĩa khai báo tiêu chuẩn của chương trình logic --- mô hình Herbrand ít nhất (nghĩa là tập hợp các thuật ngữ mặt đất được xác định theo cảm tính) . Trong công tác lý thuyết về lập trình logic, đây thường là đối tượng nghiên cứu và được biết rằng một câu trả lời hoàn chỉnh và âm thanh cho các truy vấn có thể đạt được (theo nghĩa "đệ quy-enumerable"), ví dụ, sử dụng độ phân giải SLD tùy thuộc vào các điều kiện sau:
- công bằng tìm kiếm cho phù hợp với quy định (ví dụ, tìm kiếm theo chiều sâu Prolog là không công bằng);
- hợp nhất với "xảy ra-kiểm tra" (kiểm tra xem biến không xảy ra trong cụm từ được hợp nhất).
Tôi đang tìm một triển khai ngắn gọn sẽ xây dựng trên các khả năng hiện có, thay vì phát minh ra bánh xe. Hai trong số các hướng dẫn đầy hứa hẹn hơn mà tôi thấy đang thực hiện nó như một siêu thông dịch viên của Prolog, hoặc là một phần của một số định lý tục ngữ. Bất cứ ai có kiến thức thực tế trong các lĩnh vực này cung cấp một số hướng dẫn về cách thực hiện nó? Có thể dễ dàng triển khai trong miniKanren không?
Ý định của tôi là chính thức hóa một số kiến thức theo cách đầy đủ. Các đặc điểm quan trọng của việc chính thức hóa như vậy là nó tương ứng chính xác với khái niệm toán học (monotone) của toán học, để kiến thức và các thuộc tính của nó có thể dễ dàng được lý luận về các đối số quy nạp.
Câu hỏi yêu cầu chúng tôi đề xuất hoặc tìm sách, công cụ, thư viện phần mềm, hướng dẫn hoặc tài nguyên ngoài trang web khác không có chủ đề cho Stack Overflow vì chúng có xu hướng thu hút câu trả lời và spam. – Enigmativity
Tôi không tìm kiếm ý kiến. Tôi yêu cầu sự giúp đỡ để tìm một thứ mà tôi không tìm được, hoặc một số hướng dẫn về cách tự làm điều đó (nói, trong [miniKanren] (http://minikanren.org/)). – amka00
@ amka00 - Đó là phần "tìm thấy" của nhận xét của tôi. – Enigmativity