The Complexity of Theorem-Proving Procedures

Tóm tắt

Chỉ ra rằng mọi bài toán nhận dạng được giải bởi một máy Turing không tất định bị giới hạn thời gian đa thức đều có thể được "rút gọn" về bài toán xác định liệu một công thức mệnh đề đã cho có phải là một hằng đúng hay không. Ở đây "rút gọn" có nghĩa, một cách đại khái, là bài toán thứ nhất có thể được giải một cách tất định trong thời gian đa thức với điều kiện có sẵn một oracle để giải bài toán thứ hai. Từ khái niệm về khả năng rút gọn này, các bậc đa thức về độ khó được định nghĩa, và chỉ ra rằng bài toán xác định tính hằng đúng có cùng bậc đa thức với bài toán xác định liệu đồ thị thứ nhất trong hai đồ thị đã cho có đẳng cấu với một đồ thị con của đồ thị thứ hai hay không. Các ví dụ khác được thảo luận. Một phương pháp đo độ phức tạp của các thủ tục chứng minh cho phép tính vị từ được đưa ra và thảo luận.

Trong toàn bộ bài báo này, một tập các chuỗi có nghĩa là một tập các chuỗi trên một bảng chữ cái $\Sigma$ cố định, lớn, hữu hạn nào đó. Bảng chữ cái này đủ lớn để bao gồm các ký hiệu cho tất cả các tập được mô tả ở đây. Tất cả các máy Turing đều là các thiết bị nhận dạng tất định, trừ khi điều ngược lại được nêu rõ.

1 Các phép đồng nhất và khả quy đa thức

Ta cố định một hình thức hóa cho phép tính mệnh đề trong đó các công thức được viết dưới dạng các chuỗi trên $\Sigma$. Vì ta sẽ cần vô hạn ký hiệu mệnh đề (nguyên tử), mỗi ký hiệu như vậy sẽ gồm một phần tử của $\Sigma$ theo sau bởi một số ở dạng ký hiệu nhị phân để phân biệt ký hiệu đó. Do đó một công thức có độ dài n chỉ có thể có khoảng $n/\log n$ ký hiệu hàm và vị từ phân biệt. Các liên kết logic là $\&$ (và), $\vee$ (hoặc), và $\neg$ (không).

Tập các phép đồng nhất (được ký hiệu bởi {tautologies}) là một tập đệ quy nào đó của các chuỗi trên bảng chữ cái này, và ta quan tâm đến bài toán tìm một cận dưới tốt cho thời gian nhận dạng có thể có của nó. Ở đây ta không đưa ra cận dưới như vậy, nhưng định lý 1 sẽ cung cấp bằng chứng rằng {tautologies} là một tập khó nhận dạng, vì nhiều bài toán có vẻ khó có thể được rút gọn về việc xác định tính đồng nhất. Khi nói rút gọn, ta có ý gần đúng rằng nếu tính đồng nhất có thể được quyết định tức thời (bởi một "tiên tri") thì các bài toán này có thể được quyết định trong thời gian đa thức. Để làm chính xác khái niệm này, ta đưa vào các máy truy vấn, giống như các máy Turing với tiên tri trong [1].

Một máy truy vấn là một máy Turing nhiều băng với một băng đặc biệt được gọi là băng truy vấn, và ba trạng thái đặc biệt lần lượt được gọi là trạng thái truy vấn, trạng thái yes, và trạng thái no. Nếu M là một máy truy vấn và T là một tập các chuỗi, thì một T-tính toán của M là một tính toán của M trong đó ban đầu M ở trạng thái ban đầu và có một chuỗi đầu vào w trên băng đầu vào, và mỗi lần M đạt đến trạng thái truy vấn thì có một chuỗi u trên băng truy vấn, và trạng thái tiếp theo mà M đạt đến là trạng thái yes nếu $u \in T$ và là trạng thái no nếu $u \notin T$. Ta hình dung một "tiên tri", biết T, đặt M vào trạng thái yes hoặc no.

Định nghĩa

Một tập S các chuỗi là P-khả quy (P là đa thức) về một tập T các chuỗi khi và chỉ khi tồn tại một máy truy vấn M nào đó và một đa thức Q(n) sao cho với mỗi chuỗi đầu vào w, T-tính toán của M với đầu vào w dừng trong vòng $Q(|w|)$ bước ($|w|$ là độ dài của w), và kết thúc ở một trạng thái chấp nhận khi và chỉ khi $w \in S$.

Không khó để thấy rằng P-khả quy là một quan hệ bắc cầu. Vì vậy quan hệ E trên các tập chuỗi, được cho bởi $(S,T)\in E$ khi và chỉ khi mỗi tập $S$ và $T$ đều P-khả quy về tập kia, là một quan hệ tương đương. Lớp tương đương chứa một tập $S$ sẽ được ký hiệu bởi $\deg(S)$ (bậc đa thức về độ khó của $S$).

Định nghĩa: Ta sẽ ký hiệu $\deg(\{0\})$ bởi $\mathcal{L}_*$, trong đó $0$ biểu thị hàm không.

Do đó $\mathcal{L}_*$ là lớp các tập có thể nhận dạng trong thời gian đa thức. $\mathcal{L}_*$ đã được thảo luận trong [2], p. 5, và là dạng tương tự trên chuỗi của lớp $\mathcal{L}$ các hàm của Cabham [3].

Bây giờ ta định nghĩa các tập chuỗi đặc biệt sau đây.

1. Bài toán đồ thị con là bài toán cho hai đồ thị vô hướng hữu hạn, xác định xem đồ thị thứ nhất có đẳng cấu với một đồ thị con của đồ thị thứ hai hay không. Một đồ thị $G$ có thể được biểu diễn bởi một chuỗi $\bar{G}$ trên bảng chữ cái $\{0,1,*\}$ bằng cách liệt kê các hàng liên tiếp của ma trận kề của nó, được phân cách bởi các dấu * . Ta ký hiệu {subgraph pairs} là tập các chuỗi $\bar{G}_1**\bar{G}_2$ sao cho $G_1$ đẳng cấu với một đồ thị con của $G_2$.

1. Bài toán đẳng cấu đồ thị sẽ được biểu diễn bởi tập, được ký hiệu là {isomorphic graphpairs}, gồm tất cả các chuỗi $\bar{G}_1**\bar{G}_2$ sao cho $G_1$ đẳng cấu với $G_2$.

1. Tập {Primes} là tập tất cả các biểu diễn nhị phân của các số nguyên tố.

1. Tập {DNF tautologies} là tập các chuỗi biểu diễn các phép đồng nhất ở dạng chuẩn tách rời.

1. Tập $D_3$ gồm các phép đồng nhất ở dạng chuẩn tách rời trong đó mỗi tuyển thức có nhiều nhất ba hội thức (mỗi hội thức là một nguyên tử hoặc phủ định của một nguyên tử).

Định lý 1: Nếu một tập $S$ các chuỗi được chấp nhận bởi một máy Turing không tất định trong thời gian đa thức, thì $S$ là P-khả quy về {DNF tautologies}.

Hệ quả: Mỗi tập trong các định nghĩa 1)-5) đều là P-khả quy về {DNF tautologies}.

Điều này là vì mỗi tập, hoặc phần bù của nó, được chấp nhận trong thời gian đa thức bởi một máy Turing không tất định nào đó.

Chứng minh định lý: Giả sử một máy Turing không tất định $M$ chấp nhận một tập $S$ các chuỗi trong thời gian $Q(n)$, trong đó $Q(n)$ là một đa thức. Với một đầu vào $w$ cho $M$, ta sẽ xây dựng một công thức mệnh đề $A(w)$ ở dạng chuẩn hội sao cho $A(w)$ thỏa được khi và chỉ khi $M$ chấp nhận $w$. Do đó $\neg\neg A(w)$ dễ dàng được đưa về dạng chuẩn tách rời (sử dụng các luật De Morgan), và $\neg A(w)$ là một phép đồng nhất khi và chỉ khi $w\not\in S$. Vì toàn bộ phép xây dựng có thể được thực hiện trong thời gian bị chặn bởi một đa thức theo $|w|$ (độ dài của $w$), định lý được chứng minh.

Chúng ta có thể giả sử rằng máy Turing $M$ chỉ có một băng, vô hạn về phía bên phải nhưng có một ô ngoài cùng bên trái. Ta đánh số các ô từ trái sang phải $1, 2, \ldots$. Ta cố định một đầu vào $w$ cho $M$ có độ dài $n$, và giả sử $w\in S$. Khi đó có một phép tính của $M$ với đầu vào $w$ kết thúc ở một trạng thái chấp nhận trong vòng $T = Q(n)$ bước. Công thức $A(w)$ sẽ được xây dựng từ nhiều ký hiệu mệnh đề khác nhau, có ý nghĩa dự định, được liệt kê dưới đây, đề cập đến một phép tính như vậy.

Giả sử bảng chữ cái băng của $M$ là $\{\sigma_1, \ldots, \sigma_\ell\}$, và tập các trạng thái là $\{q_1, \ldots, q_s\}$. Lưu ý rằng vì phép tính có nhiều nhất $T = Q(n)$ bước, không có ô băng nào vượt quá số $T$ được quét.

Các ký hiệu mệnh đề:

$p_{s,t}^i$ đúng khi và chỉ khi ô băng số $s$ tại bước $t$ chứa ký hiệu $\sigma_i$.

Công thức $A(w)$ là một liên kết hội B\&C\&D\&E\&F\&G\&H\&I được tạo thành như sau. Lưu ý $A(w)$ ở dạng chuẩn hội.

B sẽ khẳng định rằng ở mỗi bước t, một và chỉ một ô được quét. B là một phép hội $B_1 \land B_2 \land \ldots \land B_T$, trong đó $B_t$ khẳng định rằng tại thời điểm t một và chỉ một ô được quét:

Với $1 \leq s \leq T$ và $1 \leq t \leq T_j$, $C_{s,t}$ khẳng định rằng tại ô s và thời điểm t có một và chỉ một ký hiệu. C là phép hội của tất cả các $C_{s,t}$.

D khẳng định rằng với mỗi t có một và chỉ một trạng thái.

E khẳng định rằng các điều kiện ban đầu được thỏa mãn:

trong đó $w = \sigma_{i_1} \cdots \sigma_{i_n}$, $q_0$ là trạng thái ban đầu và $\sigma_1$ là ký hiệu trống.

F, G, và H khẳng định rằng với mỗi thời điểm t các giá trị của các P, Q và S được cập nhật đúng. Ví dụ, G là phép hội theo mọi t, i, j của $G_{i,j}^t$, trong đó $G_{i,j}^t$ khẳng định rằng nếu tại thời điểm t máy ở trạng thái $q_i$ đang quét ký hiệu $\sigma_j$, thì tại thời điểm $t + 1$ máy ở trạng thái $q_k$, trong đó $q_k$ là trạng thái được cho bởi hàm chuyển của M.

Cuối cùng, công thức I khẳng định rằng máy đạt đến trạng thái chấp nhận tại một thời điểm nào đó. Máy M nên được sửa đổi để nó tiếp tục tính toán theo một cách tầm thường sau khi đạt đến trạng thái chấp nhận, sao cho $A(w)$ sẽ được thỏa mãn.

Bây giờ có thể dễ dàng kiểm chứng rằng $A(w)$ có tất cả các tính chất được khẳng định trong đoạn đầu tiên của chứng minh.

Định lý 2: Các tập sau đây P-giảm được lẫn nhau theo từng cặp (và do đó mỗi tập có cùng bậc khó khăn đa thức): {tautologies}, {DNF tautologies}, $D_3$, {subgraph pairs}.

Nhận xét: Chúng tôi chưa thể thêm {primes} hoặc {isomorphic graph pairs} vào danh sách trên. Việc chỉ ra rằng {tautologies} là P-giảm được về {primes} dường như đòi hỏi một số kết quả sâu sắc trong lý thuyết số, trong khi việc chỉ ra rằng {tautologies} là P-giảm được về {isomorphic graph pairs} có lẽ sẽ bác bỏ một phỏng đoán của Corneil [4] mà từ đó ông suy ra rằng bài toán đẳng cấu đồ thị có thể được giải trong thời gian đa thức.

Tình cờ, không khó để thấy từ thủ tục Davis-Putnam [5] rằng tập $D_2$, bao gồm tất cả các hằng đúng DNF với nhiều nhất hai hội tử trong mỗi tuyển tử, nằm trong $\mathcal{L}^*$. Do đó $D_2$ không thể được thêm vào danh sách trong định lý 2 (trừ khi tất cả các tập trong danh sách đều nằm trong $\mathcal{L}^*$).

Chứng minh định lý 2: Theo hệ quả của định lý 1, mỗi tập đều P-giảm được về {DNF tautologies}. Vì hiển nhiên {DNF tautologies} là P-giảm được về {tautologies}, còn lại cần chỉ ra rằng {DNF tautologies} là P-giảm được về $D_3$ và $D_3$ là P-giảm được về {subgraph pairs}.

Để chỉ ra rằng {các hằng đúng DNF} là P-rút gọn được về $D_3$, cho A là một công thức mệnh đề ở dạng chuẩn tuyển. Giả sử $A = B_1 \lor B_2 \lor \ldots \lor B_k$, trong đó $B_1 = R_1 \land \ldots \land R_s$, và mỗi $R_i$ là một nguyên tử hoặc phủ định của một nguyên tử, và $s > 3$. Khi đó A là một hằng đúng khi và chỉ khi $A'$ là một hằng đúng, trong đó

trong đó P là một nguyên tử mới. Vì chúng ta đã giảm số hạng liên hợp trong $B_1$, quá trình này có thể được lặp lại cho đến khi cuối cùng tìm được một công thức có nhiều nhất ba hạng liên hợp trên mỗi hạng tuyển. Rõ ràng toàn bộ quá trình bị chặn về thời gian bởi một đa thức theo độ dài của A.

Còn lại cần chỉ ra rằng $D_3$ là P-rút gọn được về {các cặp đồ thị con}. Giả sử A là một công thức ở dạng chuẩn tuyển với ba hạng liên hợp trên mỗi hạng tuyển. Do đó $A = C_1 \lor \ldots \lor C_k$, trong đó

C_i = R_{i1} \& R_{i2} \& R_{i3}, và mỗi R_{ij} là một nguyên tử hoặc một phủ định của một nguyên tử. Bây giờ cho G_1 là đồ thị đầy đủ với các đỉnh {v_1, v_2, ..., v_k}, và cho G_2 là đồ thị với các đỉnh {u_{ij}}, 1 \leq i \leq k, 1 \leq j \leq 3, sao cho u_{ij} được nối bằng một cạnh với u_{rs} khi và chỉ khi i \neq r và hai literal (R_{ij}, R_{rs}) không tạo thành một cặp đối nhau (nghĩa là chúng không có dạng (P, \neg P) cũng không có dạng (\neg P, P)). Do đó tồn tại một phép gán chân trị làm sai công thức A khi và chỉ khi tồn tại một đồng cấu đồ thị $\phi : G_1 \to G_2$ sao cho với mỗi i, $\phi(v_i) = u_{ij}$ với một j nào đó. (Đồng cấu cho biết với mỗi i, phần tử nào trong R_{i1}, R_{i2}, R_{i3} cần bị làm sai, và việc thiếu cạnh có chọn lọc trong G_2 đảm bảo rằng phép gán chân trị thu được được xác định nhất quán).

Để đảm bảo rằng một đồng cấu một-một $\phi : G_1 \to G_2$ có tính chất rằng với mỗi i, $\phi(v_i) = u_{ij}$ với một j nào đó, chúng ta sửa đổi G_1 và G_2 như sau. Chúng ta chọn các đồ thị H_1, H_2, ..., H_k đủ khác biệt với nhau sao cho nếu G'_1 được tạo thành từ G_1 bằng cách gắn H_i vào v_i, 1 \leq i \leq k, và G'_2 được tạo thành từ G_2 bằng cách gắn H_i vào mỗi u_{i1} và u_{i2} và u_{i3}, 1 \leq i \leq k, thì mọi đồng cấu một-một $\phi : G'_1 \to G'_2$ đều có tính chất vừa nêu. Không khó để thấy rằng một cấu tạo như vậy có thể được thực hiện trong thời gian đa thức. Khi đó G'_1 có thể được nhúng vào G'_2 khi và chỉ khi A \notin D_3. Điều này hoàn thành chứng minh của định lý 2.

2 Thảo luận

Định lý 1 và hệ quả của nó cung cấp bằng chứng mạnh mẽ rằng không dễ xác định liệu một công thức mệnh đề đã cho có phải là một hằng đúng hay không, ngay cả khi công thức đó ở dạng tuyển chuẩn tắc. Định lý 1 và 2 cùng nhau gợi ý rằng việc tìm kiếm một thủ tục quyết định đa thức cho bài toán đồ thị con là vô ích, vì thành công sẽ đưa các thủ tục quyết định đa thức đến nhiều bài toán khác có vẻ không khả thi. Dĩ nhiên nhận xét tương tự áp dụng cho bất kỳ bài toán tổ hợp nào mà {tautologies} là P-reducible.

Hơn nữa, các định lý gợi ý rằng {tautologies} là một ứng viên tốt cho một tập thú vị không thuộc $\mathcal{L}^*$, và tôi cảm thấy đáng để dành nỗ lực đáng kể nhằm chứng minh phỏng đoán này. Một chứng minh như vậy sẽ là một đột phá lớn trong lý thuyết độ phức tạp.

Xét đến độ phức tạp rõ ràng của {DNF tautologies}, việc khảo sát thủ tục Davis-Putnam [5] là điều thú vị. Thủ tục này được thiết kế để xác định liệu một công thức đã cho ở dạng hội chuẩn tắc có thỏa được hay không, nhưng dĩ nhiên thủ tục "đối ngẫu" xác định liệu một công thức đã cho ở dạng tuyển chuẩn tắc có phải là một hằng đúng hay không. Cho đến nay tôi vẫn chưa thể tìm được một dãy ví dụ cho thấy thủ tục này (được xử lý một cách thích hợp để tránh một số cạm bẫy nhất định) phải cần nhiều hơn thời gian đa thức. Tôi cũng chưa tìm thấy một cận trên thú vị cho thời gian cần thiết.

Nếu ta cho phép các chuỗi biểu diễn các số tự nhiên, (hoặc các bộ k của các số tự nhiên) sử dụng ký hiệu m-adic hoặc ký hiệu thích hợp khác, thì các khái niệm trong các phần trước có thể được áp dụng cho các tập số (hoặc các quan hệ k-vị trí trên các số). Không khó để thấy rằng tập các quan hệ được chấp nhận trong thời gian đa thức bởi một máy Turing không tất định chính là tập $\mathcal{L}^+$ gồm các quan hệ có dạng

(1) $(\exists y \leq g_k(\bar{x}))\ R(\bar{x},y)$ trong đó $g_k(\bar{x}) = 2^{(\ell(\max \bar{x}))^k}$, $\ell(z)$ là độ dài dyadic của z, và $R(\bar{x}, y)$ là một quan hệ $\mathcal{L}^*$, ($\mathcal{L}^+$ là lớp các quan hệ sơ đẳng dương mở rộng của Bennett [6]). Nếu ta loại bỏ cận trên của lượng từ trong công thức (1), lớp $\mathcal{L}^+$ sẽ trở thành lớp các tập đệ quy đếm được. Vì vậy nếu $\mathcal{L}^+$ là tương tự của lớp các tập r.e., thì việc xác định tautologyhood là tương tự của bài toán dừng; vì, theo định lý 1, {tautologies} có bậc $\mathcal{L}^+$ đầy đủ giống như bài toán dừng có bậc r.e. đầy đủ. Đáng tiếc, lập luận đường chéo cho thấy bài toán dừng không đệ quy dường như không thể được điều chỉnh để chứng minh {tautologies} không thuộc $\mathcal{L}^*$.

3 Phép tính vị từ

Các công thức trong phép tính vị từ được biểu diễn bằng các chuỗi theo cách tương tự như phép tính mệnh đề. Ngoài các ký hiệu của phép tính mệnh đề, chúng ta cần các ký hiệu lượng từ $\forall$ và $\exists$, cùng các ký hiệu để tạo thành danh sách vô hạn các biến cá thể, và các danh sách vô hạn các ký hiệu hàm và vị từ của mỗi cấp (tất nhiên bảng chữ cái cơ sở $\Sigma$ vẫn là hữu hạn).

Giả sử Q là một thủ tục hoạt động trên các công thức trên và kết thúc trên một công thức đầu vào đã cho A khi và chỉ khi A không thỏa được. Vì không có thủ tục quyết định cho tính thỏa được trong phép tính vị từ, suy ra không có hàm đệ quy T sao cho nếu A không thỏa được, thì Q sẽ kết thúc trong vòng T(n) bước, với n là độ dài của A. Vậy làm thế nào để đánh giá hiệu quả của thủ tục?

Chúng ta sẽ sử dụng cách tiếp cận sau. Hầu hết các bộ chứng minh định lý tự động phụ thuộc vào định lý Herbrand, phát biểu ngắn gọn rằng một công thức A không thỏa được khi và chỉ khi một số phép hội của các thể hiện thay thế của dạng hàm fn(A) của A là không nhất quán theo hàm chân trị. Giả sử chúng ta sắp thứ tự các hạng trong vũ trụ Herbrand của fn(A) theo hạng, rồi sắp xếp theo một cách tự nhiên các thể hiện thay thế của fn(A) từ vũ trụ Herbrand. Thứ tự này nên sao cho nói chung các thể hiện thay thế sử dụng các hạng có hạng lớn hơn sẽ theo sau các thể hiện thay thế sử dụng các hạng nhỏ hơn. Gọi $A_1, A_2, ...$ là các thể hiện thay thế này theo thứ tự.

Định nghĩa: Nếu A không thỏa được, thì $\phi(A)$ là k nhỏ nhất sao cho $A_1 \land A_2 \land ... \land A_k$ là không nhất quán theo hàm chân trị. Nếu A thỏa được, thì $\phi(A)$ không được định nghĩa.

Bây giờ gọi Q là thủ tục, với đầu vào A, tính chuỗi $A_1, A_2, ...$ và với mỗi i, kiểm tra xem $A_1 \land ... \land A_i$ có nhất quán theo hàm chân trị hay không. Nếu câu trả lời là không tại bất kỳ thời điểm nào, thủ tục kết thúc thành công. Khi đó rõ ràng tồn tại một T(k) đệ quy sao cho với mọi k và mọi công thức A, nếu độ dài của $A \leq k$ và $\phi(A) \leq k$, thì Q sẽ kết thúc trong vòng T(k) bước. Chúng tôi đề xuất rằng hàm T(k) là một thước đo hiệu quả của Q.

Để thuận tiện, tất cả các thủ tục trong phần này sẽ được thực hiện trên các máy Turing một băng, mà chúng tôi sẽ gọi đơn giản là máy.

Định nghĩa: Cho một máy $M_Q$ và hàm đệ quy $T_Q(k)$, chúng tôi nói rằng $M_Q$ thuộc kiểu Q và chạy trong thời gian $T_Q(k)$ nếu khi $M_Q$ bắt đầu với một công thức vị từ A được ghi trên băng của nó, thì $M_Q$ dừng khi và chỉ khi A không thỏa được, và với mọi k, nếu $\phi(A) \leq k$ và $|A| \leq \log_2 k$, thì $M_Q$ dừng trong vòng $T_Q(k)$ bước. Trong trường hợp này chúng tôi cũng nói rằng $T_Q(k)$ thuộc kiểu Q. Ở đây $|A|$ là độ dài của A.

Lý do cho điều kiện $|A| \leq \log_2 k$ thay vì $|A| \leq k$, là vì với điều kiện sau, việc tìm một cận dưới cho $T_Q(k)$ sẽ gần tương đương với việc tìm một cận dưới cho bài toán quyết định của phép tính mệnh đề. Đặc biệt, định lý 3A sẽ trở nên hiển nhiên và tầm thường.

Định lý 3: A) Với mọi $T_Q(k)$ thuộc kiểu Q,

là không bị chặn.

B) Tồn tại một $T_Q(k)$ thuộc kiểu Q sao cho

Phác thảo chứng minh: A). Với bất kỳ máy M nào, có thể xây dựng một công thức vị từ $A(M)$ thỏa được khi và chỉ khi M không bao giờ dừng khi bắt đầu trên một băng trống. Điều này được thực hiện theo hướng được mô tả trong Wang [7] trong chứng minh giảm bài toán dừng về bài toán quyết định của phép tính vị từ. Hơn nữa, nếu M dừng sau s bước, thì

Do đó, nếu trái với (2), $T_Q(k) = O(\sqrt{k}/\log^2 k)$, thì một sửa đổi của $M_Q$ có thể xác minh chỉ trong

bước rằng M đã dừng sau s bước (với điều kiện $m \leq \log s^2$, trong đó m là độ dài của $A(M)$). Một lập luận đường chéo (xem [8] p. 153) cho thấy điều này nói chung là không thể.

B) Máy $M_Q$ hoạt động trong thời gian $T_Q$ bằng cách tuân theo thủ tục được nêu ở đầu phần này. Lưu ý rằng công thức $A_1 \& A_2 \& \ldots \& A_k$ có độ dài $O(k \log^2 k)$, vì chúng ta có thể giả sử $|A| \leq \log k$.

Định lý 4: Nếu tập S các chuỗi được một máy không tất định chấp nhận trong thời gian $T(n) = 2^n$, và nếu $T_Q(k)$ là một hàm trung thực (nghĩa là đếm được theo thời gian thực) thuộc kiểu Q, thì tồn tại một hằng số K sao cho S có thể được nhận dạng bởi một máy tất định trong thời gian $T_Q(K8^n)$.

Chứng minh: Giả sử $M_1$ là một máy không tất định chấp nhận S trong thời gian $2^n$. Gọi $M_2$ là một máy không tất định mô phỏng $M_1$ đúng $2^n$ bước rồi dừng, trừ khi $M_1$ chấp nhận đầu vào, trong trường hợp đó $M_2$ tính toán mãi mãi. Do đó với mọi chuỗi w, nếu $w \in S$ thì tồn tại một phép tính mà trong đó $M_2$ với đầu vào w không dừng, và nếu $w \notin S$, thì $M_2$ với đầu vào w dừng trong vòng $4^n$ bước đối với mọi phép tính. Bây giờ với w có độ dài n, ta có thể xây dựng một công thức $A(w)$ có độ dài $O(n)$ sao cho $A(w)$ thỏa được khi và chỉ khi $M_1$ chấp nhận w. ($A(w)$ được xây dựng theo cách tương tự như $A(M)$ trong chứng minh của 1A). Hơn nữa, nếu $M_2$ dừng trong vòng $4^n$ bước đối với mọi phép tính có thể có, thì

Do đó, có thể xây dựng một máy tất định M để xác định liệu $w \in S$ hay không bằng cách cung cấp $M_Q$ với đầu vào $A(w)$. Nếu không có kết quả nào xuất hiện trong vòng $T_Q(K8^n)$ bước, thì $w \in S$, và ngược lại $w \notin S$.

4 Thảo luận thêm:

Có một khoảng cách lớn giữa cận dưới $\sqrt{k}/(\log k)^2$ đối với các hàm thời gian $T_Q(k)$ được đưa ra trong định lý 3A và một

có thể có được trong 3B. Tuy nhiên, có những lý do cho khoảng cách này. Chẳng hạn, nếu chúng ta có thể cải thiện kết quả trong 3B và tìm được một $T_Q(k)$ bị chặn bởi một đa thức theo k, thì theo định lý 4 chúng ta có thể mô phỏng một máy bị chặn thời gian $2^n$ không tất định một cách tất định trong thời gian $p(2^n)$ với một đa thức p nào đó. Điều này trái với kinh nghiệm cho thấy mô phỏng tất định một máy bị chặn thời gian $T(n)$ không tất định nói chung đòi hỏi thời gian $k^{T(n)}$.

Mặt khác, nếu chúng ta có thể nâng cận dưới được đưa ra trong định lý 3A và chứng minh rằng

là không bị chặn, thì chúng ta có thể kết luận {Tautologies} $\notin \mathcal{L}^*$, vì nếu không thì thủ tục chứng minh Herbrand tổng quát sẽ cung cấp một $T_Q(k)$ nhỏ hơn $2^k$. Do đó, một cải thiện như vậy trong 3A sẽ đòi hỏi một bước đột phá lớn trong lý thuyết độ phức tạp.

Lĩnh vực chứng minh định lý cơ học rất cần một cơ sở để so sánh và đánh giá hàng chục thủ tục xuất hiện trong tài liệu. Hiệu năng của một thủ tục trên các ví dụ bằng máy tính là một tiêu chí tốt, nhưng không đủ (trừ khi thủ tục chứng minh được tính hữu dụng theo một cách thực tiễn nào đó). Cần có một tiêu chí độ phức tạp lý thuyết để làm nổi bật các giới hạn cơ bản và đề xuất những mục tiêu mới cần theo đuổi.

Tiêu chí được đề xuất ở đây (hàm $T_Q(k)$) có lẽ là quá thô. Chẳng hạn, có thể tốt hơn nếu biến $T_Q(k)$ thành một hàm của nhiều biến, trong đó một biến là $\phi(A)$, và một biến khác có thể là số tối thiểu các thể hiện phép thế của $fn(A)$ cần thiết để tạo thành một mâu thuẫn (lưu ý rằng nói chung không phải tất cả các $A_1, A_2, \ldots, A_{\phi(A)}$ đều cần thiết.)

$T_Q(k)$ có thể là một phép đo thô, nhưng nó cung cấp một cơ sở cho thảo luận, và tôi hy vọng sẽ kích thích tiến bộ hướng tới việc tìm ra các phép đo độ phức tạp tốt hơn cho các hệ chứng minh định lý.