xây dựng hệ thống giải bài toán smt hiệu năng cao – phần máy trạm

LINK DOWNLOAD MIỄN PHÍ TÀI LIỆU "xây dựng hệ thống giải bài toán smt hiệu năng cao – phần máy trạm": http://123doc.vn/document/1044852-xay-dung-he-thong-giai-bai-toan-smt-hieu-nang-cao-phan-may-tram.htm

Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
5.2.2.8.

Lớp Term 24

5.2.2.9.

Lớp annotation 24

5.2.2.10.

Lớp varDecl 24

5.2.2.11.

Lớp fvarDecl 24

5.2.2.12.

Lớp Arith_symb 25

5.2.2.13.

Lớp Identifier 25

5.2.2.14.

Lớp quant_var 25

5.3.

Phần máy trạm 26

5.3.1.

Cơ chế làm việc của máy trạm 26

5.3.2.

Quy định giao tiếp với máy chủ 27

5.3.3.

Hoạt động của hệ thống máy trạm 28

5.3.4.

Các lớp của hệ thống máy trạm 30

5.3.4.1.

Biểu đồ lớp của hệ thống 30

5.3.4.2.

Lớp config 30

5.3.4.3.

Lớp sessionID 30

5.3.4.4.

Lớp Solver 31

5.3.4.5.

Lớp ReadThread 31

5.3.4.6.

Lớp WriteThread 34

5.4.

Tổng kết 34

Chương 6.

Cài đặt và thử nghiệm 36

6.1.

Cài đặt 36

6.2.

Bài toán thực nghiệm 36

6.2.1.

Xây dựng bài toán SMT dựa trên các hàm API 36

6.2.2.

Thử nghiệm kết nối với máy chủ và toàn hệ thống 37

Hướng phát triển tiếp theo của hệ thống 40


Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Danh sách các bảng trong tài liệu
Bảng 1: Luật sinh một toán hạng 7

Bảng 2: Luật sinh một công thức 8

Bảng 3: Luật sinh một thuyết 8

Bảng 4: Luật sinh một logic 8

Bảng 5 Luật sinh một chuẩn 9

Bảng 6: Các lý thuyết nền được quy chuẩn trong SMT-LIB 1.2 9

Bảng 7: Các Logic quy chuẩn được đưa ra trong SMT-LIB 1.2 10

Bảng 8 Bảng dữ liệu các tệp tin đầu vào thử nghiệm 37

Bảng 9: Kết quả thời gian của thực nghiệm 37

Bảng 10: Kêt quả trả về của thực nghiệm 38

Danh sách các hình trong tài liệu
Hình 3.1 Mô hình hệ thống giải bài toán SMT hiệu năng cao. 12

Hình 3.2: Mô hình ca sử dụng của hệ thống 14

Hình 3.3: Mô hình hoạt động của hệ thống 15

Hình 5.1: Biểu đồ lớp của hệ thống máy trạm 30

Danh sách từ viết tắt trong tài liệu
Từ viết tắt Từ chuẩn Diễn giải
SMT Satisfiability Modulo Theories
Các lý thuyết module về
tính thỏa được
SMT-LIB
Satisfiability Modulo Theories -
Liblary
Thư viện các lý thuyết
module về tính thỏa được
API
Application Programming
Interface
Giao diện lập trình ứng
dụng


Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 1
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Chương 1. Mở đầu
1.1. Giới thiệu
Hiện nay, cùng với sự phát triển bùng nổ của hầu hết các ngành khoa học,
ngành khoa học máy tính cũng có những tiến bộ to lớn. Song song với đó, nhu cần
nghiên cứu về việc giải hoặc đưa ra tính khả thi của một biểu thức logic ngày càng
được quan tâm và phát triển. Bởi lẽ, rất nhiều các ứng dụng hay những sự tính toán
trong ngành khoa học máy tính cần đến những công thức logic phức tạp. Trong
khoảng hai thập niên gần đây, ngành khoa học máy tính đã có những tiến bộ lớn đối
với việc tự động chứng minh hay bác bỏ tính đúng đắn của một biểu thức logic. Tuy
nhiên việc chứng minh các biểu thức logic sẽ khó khăn hơn nhiều nếu đặt chúng trong
một nền lý thuyết thay vì chứng minh một cách tổng quát [1,2]. Những vấn đề này
được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo Theories
hay còn được viết tắt là SMT [1]).
Cho đến nay, nhiều trường đại học cùng những nhà nghiên cứu khoa học máy
tính đã có những nghiên cứu, sản phẩm để giải quyết vấn đề này. Tuy nhiên, việc xây
dựng một bộ giải các vấn đề SMT tối ưu cho mọi trường hợp và rất khó khăn. Vì vậy,
vấn đề được đặt ra là kết hợp các bộ giải SMT đó để có được một bộ giải tối ưu nhất
về mặt thời gian.
1.2. Bài toán đặt ra
Đối với việc giải quyết các vấn đề SMT, nhiều trường đại học cũng như các cơ
quan, tổ chức lớn trên thế giới đã có những nghiên cứu và đưa ra những sản phẩm của
mình. Tuy nhiên, với mỗi sản phẩm, họ đưa vào những thuật toán khác nhau để giải
quyết vấn đề này. Trong khuôn khổ đồ án, việc nghiên cứu cơ chế, và tính đúng đắn
của những bộ giải này không được đề cập đến (kết quả đưa ra của các bộ giải sẽ được
coi là luôn đúng đắn) mà sẽ tập trung vào việc sử dụng những bộ giải này như là
những công cụ giải quyết vấn đề SMT được đưa vào. Với những kết quả đưa ra bởi
các bộ giải này, cần có một kết trả được trả về tối ưu nhất về mặt thời gian.
Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 2
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Để giải quyết vấn đề nói trên, cần có một hệ thống phân phối các vấn đề SMT
cho các bộ giải và nhận về kết quả trả về tối ưu nhất về mặt thời gian. Ngoài ra để tiện
cho việc sử dụng và phát triển hệ thống, cần có một thư viện các hàm nhúng hỗ trợ
người sử dụng xây dựng các vấn đề SMT.
1.3. Cấu trúc nội dung tài liệu
Tài liệu này nhằm giới thiệu về bài toán SMT và mô tả hệ thống giải quyết bài
toán đó trực tuyến. Chương mở đầu của tài liệu giới thiệu qua về bài toán SMT và bài
toán đặt ra cho việc xây dựng hệ thống giải quyết bài toán SMT đó.
Chương thứ hai của tài liệu đề cập tới một số kiến thức về SMT và cấu trúc,
khuôn dạng của bài toán SMT được xây dựng theo chuẩn SMT-LIB. Chương này được
coi là kiến thức nền tảng để xây dựng hệ thống giải quyết bài toán SMT hiệu năng cao.
Những kiến thức trong chương này sẽ được sử dụng để xây dựng các hàm API cho hệ
thống máy khách và một số thành phần của hệ thống máy trạm.
Chương ba và chương bốn là phần phân tích và hướng giải quyết vấn đề xây
dựng hệ thống giải bài toán SMT hiệu năng cao. Chương ba sẽ tập trung hơn vào vấn
đề phân tích, đưa ra một cái nhìn tổng quan về hệ thống và quy trình hệ thống sẽ hoạt
động. Chương bốn sẽ là một số lựa chọn giải pháp để giải quyết một số vấn đề khi xây
dựng hệ thống.
Hệ thống giải bài toán SMT hiệu năng cao phần máy trạm và máy khách sẽ được
mô tả chi tiết trong chương năm. Ở chương này, hệ thống các hàm API trên máy khách
sẽ được mô tả rất chi tiết và có thể coi là tài liệu hướng dẫn cho người dùng sử dụng
các hàm API này.
Chương sáu sẽ đưa ra phần thực nghiệm và đánh giá kết quả của hệ thống. Trong
chương này, kết quả của một số thực nghiệm hệ thống sẽ được đưa ra nhằm đưa ra một
số ưu điểm mà hệ thống có được.

Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 3
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Chương 2. Kiến thức nền tảng
2.1. Giới thiệu SMT
Tính thỏa mãn là một trong những vấn đề quan trọng nhất của ngành khoa học
máy tính. Các vấn đề cần tính thỏa mãn được ứng dụng trong cả phát triển phần cứng
cũng như phần mềm, đặc biệt là kiểm định phần cứng, kiểm thử, lập lịch, đồ thị [3].
Trong các lĩnh vực nói trên, nhiều các ứng dụng được xây dựng dựa trên việc
tạo ra các công thức tiền tố và việc chứng minh tính hợp lệ của chúng. Cho dù hai thập
niên gần đây, việc chứng minh tính hợp lệ của các định lý, biểu thức tiền tố có những
tiến bộ đáng kể, tuy nhiên, không phải công thức nào cũng có thể chứng minh một
cách tự động được. Lý do của vấn đề này là bởi lẽ nhiều công thức không quan tâm
đến tính khả thi trong trường hợp tổng quát mà chỉ được quan tâm trong một lý thuyết
nền tảng [2,1]. Việc nghiên cứu tính khả thi của các công thức trong một lý thuyết nền
tảng được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo
Theories hay SMT) và các công cụ để chứng minh một cách tự động các tính khả thi
của những vẫn đề SMT được gọi là bộ giải SMT (SMT solver).
Lý thuyết về SMT sẽ được đề cập cụ thể hơn trong phần giới thiệu về thư viện
SMT.
2.2. Bộ giải SMT (SMT solver)
Trên thực tế, việc xây dựng và sử dụng các bộ giải SMT được phát triển khá
sớm, từ đầu những năm 1980. Tại thời điểm đó, một số bộ giải được xây dựng bởi
Greg Nelson và Derek Oppent tại trường đại học Stanford , Robert Shostak tại SRI, và
Robert Boyer và J Moore tại trường đại học ở Texas. Đến cuối những năm 1990, việc
nghiên cứu SMT hiện đại dựa trên lợi thế của công nghệ SAT đã xây dựng nhiều bộ
giải SMT tiến bộ hơn [4].
Như đã đề cập ở trên, trong khuôn khổ đồ án, việc đánh giá về tính đúng đắn,
các nghiên cứu về thuật giải của từng bộ giải sẽ không được đề cập đến. Vấn đề được
Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 4
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
đặt ra ở đây là kết quả của bộ giải nào sẽ được đưa ra sớm nhất. Hiện nay, có rất nhiều
các bộ giải như Absolver, Boolector, CVC3, OpenSMT, Yices, Z3…
Do yêu cầu của hệ thống là phải đưa ra được giá trị thỏa mãn (nếu bài toán
SMT đó có thỏa mãn) nên bộ giải hệ thống sử dụng phải hỗ trợ chức năng này. Ngoài
ra hệ thống sử dụng đầu vào theo chuẩn của SMT-Lib và ngắt thời gian giải một bài
toán (trong trường hợp bài toán cần thời gian giải quá lớn), do đó, bộ giải cần phải có
hỗ trợ những chức năng này khi hoạt động. Từ những yêu cầu đó, nhóm nghiên cứu và
phát triển hệ thống đã quyết định sử dụng song song hai bộ giải là Yices của SRI
International và Z3 của Microsoft. Hai bộ giải này tuy có cấu trúc khác nhau nhưng
cùng được dựa trên thuật giải DPLL (Davis-Putnam-Logemann-Loveland) [5]. Việc
tìm hiểu, phân tích cấu trúc cũng như thuật toán của hai bộ giải này sẽ không được đề
cập cụ thể ở đây.
2.3. Thư viện SMT (SMT-LIB)
Đề giải quyết các vấn đề SMT, việc nghiên cứu và đưa ra một chuẩn đầu vào là
rất cần thiết. Thông thường, mỗi bộ giải SMT đều có một quy định riêng cho chuẩn
đầu vào của mình, tuy nhiên như vậy sẽ thực sự khó khăn đối với việc thực thi một đầu
vào bởi các bộ giải khác nhau. Vì vậy, việc nghiên cứu và đưa ra một chuẩn đầu vào
thống nhất là rất cần thiết.
Khoảng tháng tư năm 2004, Silvio Rainise và Cesare Tinelli đã đưa ra chuẩn về
SMT-LIB đầu tiên [6]. Thời gian sau đó, họ liên tục cải tiến chuẩn đầu vào, bổ sung
những quy định chuẩn, thuyết mới. Cho đến nay, hai tác giả này đã và đang xây dựng
chuẩn SMT-LIB đã có phiên bản 2.0, tuy nhiên việc xây dựng đầu vào dựa trên chuẩn
mới này chưa được phổ biến. Hầu hết các bộ giải cũng như đầu vào cho các vấn đề
SMT-LIB đều được sử dụng bởi chuẩn 1.2 mà họ đã xây dựng vào khoảng tháng 8
năm 2006.
2.3.1. Cấu trúc cơ bản của SMT-LIB
Như đã nói ở trên, vấn đề SMT là việc kiểm tra biểu thức logic φ có thỏa mãn
được hay không trong lý thuyết nền T hay có một khuôn mẫu của T là khả thi. Vì vậy,
kiến trúc cơ bản của một SMT-LIB thường bao gồm các vấn đề sau [7]:
Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 5
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
- Một thủ tục logic cơ sở (underlying logic): Định dạng SMT-LIB hiện tại có hai
định nghĩa về ngữ nghĩa của logic cơ sở. Thứ nhất là dịch nghĩa sang những
biểu thức tiền tố cổ điển, có nghĩa là thủ tục của logic cơ sở giúp cho việc
chuyển đổi sang khung làm việc của công cụ có sẵn hoặc giúp kiểm tra kết quả
một cách dễ dàng hơn. Nghĩa thứ hai là chi phối ngữ nghĩa đại số dựa trên
nhiều khuôn mẫu rút gọn.
- Một lý thuyết nền (background theory): là những lý thuyết nền dùng để kiểm
chứng tính thỏa mãn. Những lý thuyết cơ bản bao gồm lý thuyết số thực, lý
thuyết mảng Phiên bản hiện tại của SMT-LIB chỉ hỗ trỡ những lý thuyết cơ
bản này.
- Một ngôn ngữ đầu vào (input language): Là lớp các biểu thức được chấp nhận
như là đầu vào của SMT-LIB.
2.3.2. Khuôn dạng của SMT-LIB
Một thư viện SMT được xây dựng theo chuẩn và dựa trên những định nghĩa sau
(theo [7]):
Định nghĩa 1 (Ký hiệu của SMT-LIB – SMT-LIB signature): Một ký hiệu SMT-
LIB Σ là một bộ dữ liệu bao gồm:
- Một tập không rỗng
∑
⊆
ௌ
ܲ các ký hiệu phân cấp (sort symbol), một tập
hợp ký hiệu hàm (function symbol)
∑
⊆
ி
ܨ và tập hợp các ký hiệu vị từ
(predicate symbol)
∑
⊆
௉
ܲ;
- Một toàn ánh (total mapping) từ các biến (term variables) X tới Σ
S
;
- Một quan hệ toàn phương (total relation) từ Σ
F
đến (Σ
S
)
+
, một chuỗi các
thành phần của Σ
S
, không bao giờ có một cặp định dạng (f,s
1
…s
n
s) và
(f,s
1
…s
n
s’) với s và s’ khác nhau;
- Một quan hệ toàn phương từ Σ
P
tới (Σ
S
)*, thứ tự các thành phần Σ
P
.
Định nghĩa 2 (Công thức trong SMT-LIB – SMT-LIB formula): Các công thức
trong ngôn ngữ SMT-LIB là một tập hợp tất cả các công thức đúng cú pháp
đóng (closed well-formed formula).
Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 6
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Định nghĩa 3 (khai báo lý thuyết – theory decl): chỉ tồn tại một khai báo lý
thuyết trong một bài toán SMT-LIB và phải thỏa mãn những giới hạn sau:
- Chúng bao gồm các khai báo của thuộc tính “sort” và “definition”;
- Chúng chứa ít nhất một khai báo với một thuộc tính;
- Không tồn tại khai báo định dạng f,s
1
…s
n
s và f,s
1
…s
n
s’ cho cùng một ký
tự hàm f mà s và s’ khác nhau;
- Tất cả các rút gọn trong khai báo ký tự hàm, vị từ được liệt kê trong khai
báo thuộc tính “sort”;
- Định nghĩa của lý thuyết được quy định trong thuộc tính “definition” và
chỉ liên quan đến các khai báo ký tự phân cấp, ký tự hàm và ký tự vị từ;
- Công thức trong thuộc tính “axiom” được xây dựng trên các khái báo ký
tự trong các thuộc tính “sort”, “funs”, “pred”.
Định nghĩa 4 (Khai báo Logic): Chỉ có một luật Logic được khai báo trong một
bài toán SMT và phải được thỏa mãn các giới hạn sau:
- Chúng bao gồm các khai báo thuộc tính “theory” và “language”;
- Chúng chứa ít nhất một khai báo đối với một thuộc tính;
- Giá trị của thuộc tính “theory” phải trùng với tên của thuyết T cho vài khai
báo của D
T
trong SMT-LIB.
Định nghĩa 5 (Khai báo về chuẩn): luật khai báo chuẩn phải thỏa mãn những
giới hạn sau:
- Chúng chứa chính xác một khai báo của thuộc tính “logic”, “formula” và
“status”;
- Giá trị của thuộc tính “logic” phải trùng khớp với tên của logic L cho vài
khai báo D
L
trong SMT-LIB;
- Mỗi một ký hiệu được khai báo trong thuộc tính “extrasorts”, “extrafuns”
và “extrapred” cần phải là một phần của các ký hiệu được định nghĩa trong
thuộc tính “language” của logic L;
- Có thể có hơn một khai báo của thuộc tính “extrasort”;
Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 7
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
- Có thể có hơn một khai báo của thuộc tính “extrafuns”, và mỗi thuộc tính
“funs” của khai báo thuyết liên kết tới D
L
phải thỏa mãn yêu cầu 3 của
định nghĩa 3;
- Ký hiệu rút gọn trong khai báo “extrafuns” hoặc “extrapred” hoặc được
khai báo trong “extrasort” hoặc thuộc về ký hiệu của logic L;
- Công thức trong khai báo thuộc tính “assumption” và “formula” là ngôn
ngữ của L và các ký hiệu của chúng được khai báo trong thuộc tính
“extrasorts” “extrafuns” và “extrapred”.
Từ những định nghĩa trên, việc xây dựng một bài toán SMT dựa trên chuẩn
SMT-LIB sẽ theo cấu trúc sau [7]:
Bảng 1: Luật sinh một toán hạng
(1)

< simple_identifier> ::= Chuỗi các ký tự, số, dấu chấm(.), nháy đơn(‘)
và g
ạ
ch dư
ớ
i , b
ắ
t đ
ầ
u b
ở
i ký t
ự

(2)

< user_value_content> ::= Bất kỳ chuỗ ký tự có thể in ra được
(3)

< user_value> ::= {< user_value_content>}
(4)

<numeral> ::= 0 | chuỗi không rỗng các chữ số bắt đầu khác 0
(5)

<rational> ::= <numeral>.0*<numeral>
(6)

<
indexed_
identifier
>

::=

<

simple_identifier
>[
<numeral>(:<numeral>)*]

(7)

<identifier> ::= <simple_identifier> | <indexed_identifier>
(8)

<var> ::= ?< simple_identifier >
(9)

<fvar> ::= $< simple_identifier >
(10)

<attribute> ::= : <simple_identifier>
(11)

<arith_symb> ::= Chuỗi không rỗng các ký tự:
=, >, <, &, @, #, +, -, *, /, %, |, ~
(12)

<funs_symb>

::=

<identifier> | <arith_symb>

(13)

<pred_symb> ::= <identifier> | <arith_symb> | distinct
(14)

<sort_symb> ::= <identifier>
(15)

<annotation> ::= <attribute> | <attribute> < user value>
(16)

<base_term> ::= <var> | <numeral> | <rational> | <identifier>
(17)

<an_term> ::= <base_term> | (<base_term> <annotation>
+
)
| (<funs_symb> <an_term>
+
<annotation>*)
| (ite <an_formula> <an_terrm> <an_term>
<annotation>*)

Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm

2010


Trang 8
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Bảng 2: Luật sinh một công thức
(1)

<prop_atom> ::= true | false | <fvar> | <identifier>
(2)

<an_atom> ::= <prop_atom> | ( <prop_atom> <annotation>
+
)
| (<pred_symb> <an_term>
+
<annotation>*)
(3)

<connective> ::= not | implies | if_then_else | and | or | xor | iff
(4)

<quant_symb>

::=

exists | forall

(5)

<quant_var> ::= ( <var> <sort_symb>)
(6)

<an_formula> ::= <an_atom>
| ( <connective> <an formula>
+
<annotation>* )
| (<quant_symb> <quant_var>
+
<an_formula>
<annotation>* )
| (let (<var> <an_term>) <an_formula> <annotation>*
)
| ( flet ( <fvar> <an_formula> ) <an_formula>
<annotation>* )

Bảng 3: Luật sinh một thuyết
(1)

<string_content> ::= chuỗi liên tiếp các ký tự
(2)

<string> ::= “<string_content>”
(3)

<fun_symb_decl> ::= (<func_symb> <sort_symb>
+
<annotation>*)
| (<numeral> <sort_symb> <annotation>*)
| (<rational> <sort_sumb> <annotation>*)
(4)

<pred_symb_decl> ::= (<pred_symb> <sort_symb>* <annotation>*)
(5)

<theory_name> ::= <identifier>
(6)

<theory_attribute> ::= :sort ( <sort_symb>
+
)
| :funs (<fun_symb_decl>
+
)
| :preds (<pred_symb_decl>)
| :definition <string>
| :axioms <string>
| <annotation>
(7)

<theory> ::= (theory <theory_name> <theory_atrribute>
+
)

Bảng 4: Luật sinh một logic
(1)

<logic_name> ::= <identifier>
(2)

<logic_attribute> ::= : theory <theory_name>
| :language <string>
| :extensions <string>
| :notes <string>