Nhan đề chính: Automated Reasoning
Nhan đề dịch: Suy luận tự động
Tác giả: Jasmin Blanchette, Laura Kovács, Dirk Pattinson
Nhà xuất bản: Springer Cham
Năm xuất bản: 2022
Số trang: 771 tr.
Ngôn ngữ: Tiếng Anh
ISBN: 978-3-031-10769-6
SpringerLink
  Lời giới thiệu: Tập này, LNAI 13385, tập hợp các bài viết của Hội nghị chung quốc tế lần thứ 11 về suy luận tự động, IJCAR 2022, được tổ chức tại Haifa, Israel, vào tháng 8 năm 2022.
32 bài nghiên cứu đầy đủ và 9 bài báo ngắn được trình bày cùng với hai bài nói chuyện được mời đã được xem xét và lựa chọn cẩn thận từ 85 bài nộp. Các bài viết tập trung vào các chủ đề: Tính thỏa mãn được, giải hệ sử dụng SMT, số học; giải tích và sắp thứ tự; trình diễn tri thức và sự minh trứng; lựa chọn, bất biến, thay thế và hình thức hóa; logic phương thức; hệ thống bằng chứng và tìm kiếm bằng chứng; các vấn đề về tiến hóa, điểm kết thúc và quyết định.
  Từ khóa: Trí tuệ nhân tạo, lý thuyết máy tự động, phần cứng máy tính, khoa học máy tính, kỹ thuật phần mềm, thiết kế phần mềm, kiến trúc phần mềm, lập trình logic, logic chính thức, ngôn ngữ chính thức, hệ thống nhúng, lập trình logic, suy luận tự động
Nội dung cuốn sách gồm những phần sau:
Bài nói chuyện của khách mời:
- Sử dụng các kỹ thuật suy luận tự động để nâng cao hiệu quả và tính bảo mật của hợp đồng thông minh (Ethereum)
- Từ tính phổ quát của chân lý toán học đến khả năng tương tác của các hệ thống chứng minh
Sự hài lòng, giải hệ sử dụng SMT và số học:
- Sản xuất bằng chứng linh hoạt trong bộ giải SMT cường độ công nghiệp
- CTL \(^*\) Kiểm tra mô hình cho các hệ thống động nhận biết dữ liệu bằng số học
- Tìm kiếm bằng chứng dựa trên SAT trong logic mệnh đề trung gian
- Khoản dự phòng và tiền xử lý ở mức thỏa mãn tối đa
- Các kỹ thuật hợp tác để giải số học thực phi tuyến tính trong bộ giải cvc5 SMT (Mô tả hệ thống)
- Tiền xử lý các mệnh đề dự phòng lan truyền
- Suy luận về vectơ bằng cách sử dụng lý thuyết trình tự SMT
Phép tính và thứ tự:
- Đường ống thử nghiệm tổng hợp hiệu quả cho các mệnh đề BS(LRA)
- Khả năng nối đất và tính liên kết trong phép tính chồng chất
- Kết nối-bắt cóc tối thiểu ở EL thông qua dịch sang FOL
- Mức độ liên quan về ngữ nghĩa
- SCL(EQ): SCL cho logic bậc nhất có đẳng thức
- Đặt hàng thuật ngữ cho việc viết lại (có điều kiện) không thể truy cập được
Trình bày tri thức và chứng minh:
- Evonne: Trực quan hóa bằng chứng tương tác cho logic mô tả (Mô tả hệ thống)
- Các hành động đối với cơ sở tri thức đóng lõi
- GK: Triển khai đầy đủ logic mặc định theo thứ tự đầu tiên cho suy luận thông thường (Mô tả hệ thống)
- Quy tắc suy luận dựa trên siêu đồ thị để tính toán \(\mathcal{EL}\mathcal{}^+\)  - Bản thể học biện minh
Lựa chọn, bất biến, thay thế và hình thức hóa:
- Phép tính tuần tự cho logic lựa chọn
- Lash 1.0 (Mô tả hệ thống)
- Goéland: Trình chứng minh định lý dựa trên Tableau đồng thời (Mô tả hệ thống)
- Mã nhị phân không bảo toàn tính nguyên thủy
- Đơn giản hóa công thức thông qua phát hiện bất biến bằng các loại được lập chỉ mục đại số
- Tableaux tổng hợp: Heuristic tìm kiếm Tableau tối thiểu
Logic phương thức:
- Logic phương thức Gödel siêu nhất quán
- Logic tuyến tính đa phương thức không kết hợp, không giao hoán
- Ngữ nghĩa hiệu quả cho logic phương thức K và KT thông qua ma trận không xác định
- Giảm cục bộ cho khối phương thức
Hệ thống bằng chứng và tìm kiếm bằng chứng:
- Chứng minh tuần hoàn, siêu dãy và logic bao đóng chuyển tiếp
- Hợp nhất và đối sánh phương trình và Phân tích khả năng tiếp cận tượng trưng trong Maude 3.2 (Mô tả hệ thống)
- Bản thể học của Leśniewski - Đặc tính chứng minh lý thuyết
- Xếp hạng Bayes cho lập kế hoạch chiến lược trong chứng minh định lý tự động
- Một khuôn khổ cho khái quát hóa gần đúng trong các lý thuyết định lượng
- Hướng dẫn chứng minh định lý tự động bằng cách viết lại thần kinh
- Đặt lại và đệ quy dựa trên đổi tên cho cú pháp với các ràng buộc
- Hệ thống bằng chứng hai chiều hữu hạn cho logic tiên đề không hữu hạn
- Ma cà rồng trở nên ồn ào: Liệu các bit ngẫu nhiên có giúp chinh phục được sự hỗn loạn? (Sự mô tả hệ thống)
Các vấn đề về tiến hóa, chấm dứt và quyết định:
- Về tính khẳng định và tính không phủ định cuối cùng đối với tổng lũy thừa có trọng số của ma trận
- Các vấn đề quyết định trong logic để suy luận về các hệ thống phân tán có thể cấu hình lại
- Chứng minh giới hạn không kết thúc và thời gian chạy thấp hơn với LoAT (Mô tả hệ thống)
- Định nghĩa ngầm định với phương trình vi phân cho Keymaera X
- Phân tích độ phức tạp tự động của các chương trình số nguyên thông qua các vòng lặp phi tuyến tính yếu hình tam giác