The Complexity of Theorem-Proving Procedures

Độ phức tạp của các thủ tục chứng minh định lý

Stephen A. Cook University of Toronto

Tóm tắt

Summary

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.

It is shown that any recognition problem solved by a polynomial time-bounded nondeterministic Turing machine can be "reduced" to the problem of determining whether a given propositional formula is a tautology. Here "reduced" means, roughly speaking, that the first problem can be solved deterministically in polynomial time provided an oracle is available for solving the second. From this notion of reducible, polynomial degrees of difficulty are defined, and it is shown that the problem of determining tautologyhood has the same polynomial degree as the problem of determining whether the first of two given graphs is isomorphic to a subgraph of the second. Other examples are discussed. A method of measuring the complexity of proof procedures for the predicate calculus is introduced and discussed.

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õ.

Throughout this paper, a set of strings means a set of strings on some fixed, large, finite alphabet $\Sigma$. This alphabet is large enough to include symbols for all sets described here. All Turing machines are deterministic recognition devices, unless the contrary is explicitly stated.

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

1 Tautologies and Polynomial Reducibility

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).

Let us fix a formalism for the propositional calculus in which formulas are written as strings on $\Sigma$. Since we will require infinitely many proposition symbols (atoms), each such symbol will consist of a member of $\Sigma$ followed by a number in binary notation to distinguish that symbol. Thus a formula of length n can only have about $n/\log n$ distinct function and predicate symbols. The logical connectives are $\&$ (and), $\vee$ (or), and $\neg$ (not).

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].

The set of tautologies (denoted by {tautologies}) is a certain recursive set of strings on this alphabet, and we are interested in the problem of finding a good lower bound on its possible recognition times. We provide no such lower bound here, but theorem 1 will give evidence that {tautologies} is a difficult set to recognize, since many apparently difficult problems can be reduced to determining tautologyhood. By reduced we mean, roughly speaking, that if tautologyhood could be decided instantly (by an "oracle") then these problems could be decided in polynomial time. In order to make this notion precise, we introduce query machines, which are like Turing machines with oracles in [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.

A query machine is a multitape Turing machine with a distinguished tape called the query tape, and three distinguished states called the query state, yes state, and no state, respectively. If M is a query machine and T is a set of strings, then a T-computation of M is a computation of M in which initially M is in the initial state and has an input string w on its input tape, and each time M assumes the query state there is a string u on the query tape, and the next state M assumes is the yes state if $u \in T$ and the no state if $u \notin T$. We think of an "oracle", which knows T, placing M in the yes state or no state.

Định nghĩa

Definition

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$.

A set S of strings is P-reducible (P for polynomial) to a set T of strings iff there is some query machine M and a polynomial Q(n) such that for each input string w, the T-computation of M with input w halts within $Q(|w|)$ steps ($|w|$ is the length of w), and ends in an accepting state iff $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$).

It is not hard to see that P-reducibility is a transitive relation. Thus the relation E on sets of strings, given by $(S,T)\in E$ iff each of $S$ and $T$ is P-reducible to the other, is an equivalence relation. The equivalence class containing a set $S$ will be denoted by $\deg(S)$ (the polynomial degree of difficulty of $S$).

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

Definition: We will denote $\deg(\{0\})$ by $\mathcal{L}_*$, where $0$ denotes the zero function.

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].

Thus $\mathcal{L}_*$ is the class of sets recognizable in polynomial time. $\mathcal{L}_*$ was discussed in [2], p. 5, and is the string analog of Cabham's class $\mathcal{L}$ of functions [3].

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

We now define the following special sets of strings.

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. The subgraph problem is the problem given two finite undirected graphs, determine whether the first is isomorphic to a subgraph of the second. A graph $G$ can be represented by a string $\bar{G}$ on the alphabet $\{0,1,*\}$ by listing the successive rows of its adjacency matrix, separated by *'s. We let {subgraph pairs} denote the set of strings $\bar{G}_1**\bar{G}_2$ such that $G_1$ is isomorphic to a subgraph of $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. The graph isomorphism problem will be represented by the set, denoted by {isomorphic graphpairs}, of all strings $\bar{G}_1**\bar{G}_2$ such that $G_1$ is isomorphic to $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. The set {Primes} is the set of all binary notations for prime numbers.

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. The set {DNF tautologies} is the set of strings representing tautologies in disjunctive normal form.

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ử).

1. The set $D_3$ consists of those tautologies in disjunctive normal form in which each disjunct has at most three conjuncts (each of which is an atom or negation of an atom).

Đị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}.

Theorem 1: If a set $S$ of strings is accepted by some nondeterministic Turing machine within polynomial time, then $S$ is P-reducible to {DNF tautologies}.

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

Corollary: Each of the sets in definitions 1)-5) is P-reducible to {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 đó.

This is because each set, or its complement, is accepted in polynomial time by some nondeterministic Turing machine.

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.

Proof of the theorem: Suppose a nondeterministic Turing machine $M$ accepts a set $S$ of strings within time $Q(n)$, where $Q(n)$ is a polynomial. Given an input $w$ for $M$, we will construct a proposition formula $A(w)$ in conjunctive normal form such that $A(w)$ is satisfiable iff $M$ accepts $w$. Thus $\neg\neg A(w)$ is easily put in disjunctive normal form (using De Morgan's laws), and $\neg A(w)$ is a tautology if and only if $w\not\in S$. Since the whole construction can be carried out in time bounded by a polynomial in $|w|$ (the length of $w$), the theorem will be proved.

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.

We may as well assume the Turing machine $M$ has only one tape, which is infinite to the right but has a left-most square. Let us number the squares from left to right $1, 2, \ldots$. Let us fix an input $w$ to $M$ of length $n$, and suppose $w\in S$. Then there is a computation of $M$ with input $w$ that ends in an accepting state within $T = Q(n)$ steps. The formula $A(w)$ will be built from many different proposition symbols, whose intended meanings, listed below, refer to such a computation.

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.

Suppose the tape alphabet for $M$ is $\{\sigma_1, \ldots, \sigma_\ell\}$, and the set of states is $\{q_1, \ldots, q_s\}$. Notice that since the computation has at most $T = Q(n)$ steps, no tape square beyond number $T$ is scanned.

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

Proposition symbols:

$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$.

$p_{s,t}^i$ is true iff tape square number $s$ at step $t$ contains the symbol $\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.

The formula $A(w)$ is a conjunctive B\&C\&D\&E\&F\&G\&H\&I formed as follows. Notice $A(w)$ is in conjunctive normal form.

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:

B will assert that at each step t, one and only one square is scanned. B is a conjunction $B_1 \land B_2 \land \ldots \land B_T$, where $B_t$ asserts that at time t one and only one square is scanned:

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}$.

For $1 \leq s \leq T$ and $1 \leq t \leq T_j$, $C_{s,t}$ asserts that at square s and time t there is one and only one symbol. C is the conjunction of all the $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.

D asserts that for each t there is one and only one state.

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

E asserts the initial conditions are satisfied:

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.

where $w = \sigma_{i_1} \cdots \sigma_{i_n}$, $q_0$ is the initial state and $\sigma_1$ is the blank symbol.

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.

F, G, and H assert that for each time t the values of the P's, Q's and S's are updated properly. For example, G is the conjunction over all t, i, j of $G_{i,j}^t$, where $G_{i,j}^t$ asserts that if at time t the machine is in state $q_i$ scanning symbol $\sigma_j$, then at time $t + 1$ the machine is in state $q_k$, where $q_k$ is the state given by the transition function for 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.

Finally, the formula I asserts that the machine reaches an accepting state at some time. The machine M should be modified so that it continues to compute in some trivial fashion after reaching an accepting state, so that $A(w)$ will be satisfied.

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.

It is now straightforward to verify that $A(w)$ has all the properties asserted in the first paragraph of the proof.

Đị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}.

Theorem 2: The following sets are P-reducible to each other in pairs (and hence each has the same polynomial degree of difficulty): {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.

Remark: We have not been able to add either {primes} or {isomorphic graph pairs} to the above list. To show {tautologies} is P-reducible to {primes} would seem to require some deep results in number theory, while showing {tautologies} is P-reducible to {isomorphic graph pairs} would probably upset a conjecture of Corneil's [4] from which he deduces that the graph isomorphism problem can be solved in polynomial time.

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}^*$).

Incidently, it not hard to see from the Davis-Putnam procedure [5] that the set $D_2$, consisting of all DNF tautologies with at most two conjuncts per disjunct, is in $\mathcal{L}^*$. Hence $D_2$ cannot be added to the list in theorem 2 (unless all sets in the list are in $\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}.

Proof of theorem 2: By the corollary to theorem 1, each of the sets is P-reducible to {DNF tautologies}. Since obviously {DNF tautologies} is P-reducible to {tautologies}, it remains to show {DNF tautologies} is P-reducible to $D_3$ and $D_3$ is P-reducible to {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 đó

To show {DNF tautologies} is P-reducible to $D_3$, let A be a proposition formula in disjunctive normal form. Say $A = B_1 \lor B_2 \lor \ldots \lor B_k$, where $B_1 = R_1 \land \ldots \land R_s$, and each $R_i$ is an atom or negation of an atom, and $s > 3$. Then A is a tautology if and only if $A'$ is a tautology where

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.

where P is a new atom. Since we have reduced the number of conjuncts in $B_1$, this process may be repeated until eventually a formula is found with at most three conjuncts per disjunct. Clearly the entire process is bounded in time by a polynomial in the length of 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 đó

It remains to show $D_3$ is P-reducible to {subgraph pairs}. Suppose A is a formula in disjunctive normal form with three conjuncts per disjunct. Thus $A = C_1 \lor \ldots \lor C_k$, where

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).

C_i = R_{i1} \& R_{i2} \& R_{i3}, and each R_{ij} is an atom or a negation of an atom. Now let G_1 be the complete graph with vertices {v_1, v_2, ..., v_k}, and let G_2 be the graph with vertices {u_{ij}}, 1 \leq i \leq k, 1 \leq j \leq 3, such that u_{ij} is connected by an edge to u_{rs} if and only if i \neq r and the two literals (R_{ij}, R_{rs}) do not form an opposite pair (that is they are neither of the form (P, \neg P) nor of the form (\neg P, P)). Thus there is a falsifying truth assignment to the formula A iff there is a graph homomorphism $\phi : G_1 \to G_2$ such that for each i, $\phi(v_i) = u_{ij}$ for some j. (The homomorphism tells for each i which of R_{i1}, R_{i2}, R_{i3} should be falsified, and the selective lack of edges in G_2 guarantees that the resulting truth assignment is consistently specified).

Để đả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.

In order to guarantee that a one-one homomorphism $\phi : G_1 \to G_2$ has the property that for each i, $\phi(v_i) = u_{ij}$ for some j, we modify G_1 and G_2 as follows. We select graphs H_1, H_2, ..., H_k which are sufficiently distinct from each other that if G'_1 is formed from G_1 by attaching H_i to v_i, 1 \leq i \leq k, and G'_2 is formed from G_2 by attaching H_i to each of u_{i1} and u_{i2} and u_{i3}, 1 \leq i \leq k, then every one-one homomorphism $\phi : G'_1 \to G'_2$ has the property just stated. It is not hard to see such a construction can be carried out in polynomial time. Then G'_1 can be embedded in G'_2 if and only if A \notin D_3. This completes the proof of theorem 2.

2 Thảo luận

2 Discussion

Đị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.

Theorem 1 and its corollary give strong evidence that it is not easy to determine whether a given proposition formula is a tautology, even if the formula is in normal disjunctive form. Theorems 1 and 2 together suggest that it is fruitless to search for a polynomial decision procedure for the subgraph problem, since success would bring polynomial decision procedures to many other apparently intractible problems. Of course the same remark applies to any combinatorial problem to which {tautologies} is 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.

Furthermore, the theorems suggest that {tautologies} is a good candidate for an interesting set not in $\mathcal{L}^*$, and I feel it is worth spending considerable effort trying to prove this conjecture. Such a proof would be a major breakthrough in complexity theory.

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.

In view of the apparent complexity of {DNF tautologies}, it is interesting to examine the Davis-Putnam procedure [5]. This procedure was designed to determine whether a given formula in conjunctive normal form is satisfiable, but of course the "dual" procedure determines whether a given formula in disjunctive normal form is a tautology. I have not yet been able to find a series of examples showing the procedure (treated sympathetically to avoid certain pitfalls) must require more than polynomial time. Nor have I found an interesting upper bound for the time required.

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

If we let strings represent natural numbers, (or k-tuples of natural numbers) using m-adic or other suitable notation, then the notions in the preceding sections can be made to apply to sets of numbers (or k-place relations on numbers). It is not hard to see that the set of relations accepted in polynomial time by some nondeterministic Turing machine is precisely the set $\mathcal{L}^+$ of relations of the form

(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}^*$.

(1) $(\exists y \leq g_k(\bar{x}))\ R(\bar{x},y)$ where $g_k(\bar{x}) = 2^{(\ell(\max \bar{x}))^k}$, $\ell(z)$ is the dyadic length of z, and $R(\bar{x}, y)$ is an $\mathcal{L}^*$ relation, ($\mathcal{L}^+$ is the class of extended positive rudimentary relations of Bennett [6]). If we remove the bound on the quantifier in formula (1), the class $\mathcal{L}^+$ would become the class of recursively enumerable sets. Thus if $\mathcal{L}^+$ is the analog of the class of r.e. sets, then determining tautologyhood is the analog of the halting problem; since, according to theorem 1, {tautologies} has the complete $\mathcal{L}^+$ degree just as the halting problem has the complete r.e. degree. Unfortunately, the diagonal argument which shows the halting problem is not recursive apparently cannot be adapted to show {tautologies} is not in $\mathcal{L}^*$.

3 Phép tính vị từ

3 The Predicate Calculus

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).

Formulas in the predicate calculus are represented by strings in a manner similar to the propositional calculus. In addition to the symbols for the latter, we need the quantifier symbols $\forall$ and $\exists$, and symbols for forming an infinite list of individual variables, and infinite lists of function and predicate symbols of each order (of course the underlying alphabet $\Sigma$ is still finite).

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?

Suppose Q is a procedure which operates on the above formulas and which terminates on a given input formula A iff A is unsatisfiable. Since there is no decision procedure for satisfiability in the predicate calculus, it follows that there is no recursive function T such that if A is unsatisfiable, then Q will terminate within T(n) steps, where n is the length of A. How then does one appraise the efficiency of the procedure?

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ự.

We will take the following approach. Most automatic theorem provers depend on the Herbrand theorem, which states briefly that a formula A is unsatisfiable if and only if some conjunction of substitution instances of the functional form fn(A) of A is truth functionally inconsistent. Suppose we order the terms in the Herbrand universe of fn(A) according to rank, and then order in a natural way the substitution instances of fn(A) from the Herbrand universe. The ordering should be such that in general substitution instances which use terms with greater rank follow substitution instances which use terms of lesser rank. Let $A_1, A_2, ...$ be these substitution instances in order.

Đị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.

Definition: If A is unsatisfiable, then $\phi(A)$ is the least k such that $A_1 \land A_2 \land ... \land A_k$ is truth-functionally inconsistent. If A is satisfiable, then $\phi(A)$ is undefined.

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.

Now let Q be the procedure which, given A, computes the sequence $A_1, A_2, ...$ and for each i, tests whether $A_1 \land ... \land A_i$ is truth-functionally consistent. If the answer is ever no, the procedure terminates successfully. Then clearly there is a recursive T(k) such that for all k and all formulas A, if the length of $A \leq k$ and $\phi(A) \leq k$, then Q will terminate within T(k) steps. We suggest that the function T(k) is a measure of the efficiency of 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.

For convenience, all procedures in this section will be realized on single tape Turing machines, which we shall call simply machines.

Đị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.

Definition: Given a machine $M_Q$ and recursive function $T_Q(k)$, we will say $M_Q$ is of type Q and runs within time $T_Q(k)$ provided that when $M_Q$ starts with a predicate formula A written on its tape, then $M_Q$ halts if and only if A is unsatisfiable, and for all k, if $\phi(A) \leq k$ and $|A| \leq \log_2 k$, then $M_Q$ halts within $T_Q(k)$ steps. In this case we will also say that $T_Q(k)$ is of type Q. Here $|A|$ is the length of 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.

The reason for the condition $|A| \leq \log_2 k$ instead of $|A| \leq k$, is that with the latter condition, finding a lower bound for $T_Q(k)$ would be nearly equivalent to finding a lower bound for the decision problem for the propositional calculus. In particular, theorem 3A would become obvious and trivial.

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

Theorem 3: A) For any $T_Q(k)$ of type Q,

là không bị chặn.

is unbounded.

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

B) There is a $T_Q(k)$ of type Q such that

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ì

Outline of proof: A). Given any machine M, one can construct a predicate formula $A(M)$ which is satisfiable if and only if M never halts when starting on a blank tape. This is done along the lines described in Wang [7] in the proof which reduces the halting problem to the decision problem for the predicate calculus. Further, if M halts in s steps, then

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

Thus, if, contrary to (2), $T_Q(k) = O(\sqrt{k}/\log^2 k)$, then a modification of $M_Q$ could verify in only

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ể.

steps that M halted in s steps (provided $m \leq \log s^2$, where m is the length of $A(M)$). A diagonal argument (see [8] p. 153) shows that this is impossible in general.

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$.

B) The machine $M_Q$ operates in time $T_Q$ by following the procedure outlined at the beginning of this section. Note that the formula $A_1 \& A_2 \& \ldots \& A_k$ has length $O(k \log^2 k)$, since we can assume $|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)$.

Theorem 4: If the set S of strings is accepted by a nondeterministic machine within time $T(n) = 2^n$, and if $T_Q(k)$ is an honest (i.e. real-time countable) function of type Q, then there is a constant K so S can be recognized by a deterministic machine within time $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ì

Proof: Suppose $M_1$ is a nondeterministic machine which accepts S in time $2^n$. Let $M_2$ be a nondeterministic machine which simulates $M_1$ for exactly $2^n$ steps and then halts, unless $M_1$ accepts the input, in which case $M_2$ computes forever. Thus for all strings w, if $w \in S$ then there is a computation for which $M_2$ with input w fails to halt, and if $w \notin S$, then $M_2$ with input w halts within $4^n$ steps for all computations. Now given w of length n, we may construct a formula $A(w)$ of length $O(n)$ such that $A(w)$ is satisfiable if and only if $M_1$ accepts w. ($A(w)$ is constructed in a way similar to $A(M)$ in the proof of 1A). Further, if $M_2$ halts within $4^n$ steps for all possible computations, then

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$.

Thus, a deterministic machine M can be constructed to determine whether $w \in S$ by presenting $M_Q$ with input $A(w)$. If no result appears within $T_Q(K8^n)$ steps, then $w \in S$, and otherwise $w \notin S$.

4 Thảo luận thêm:

4 More Discussion:

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

There is a large gap between the lower bound of $\sqrt{k}/(\log k)^2$ for time functions $T_Q(k)$ given in theorem 3A and a possible

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)}$.

given in 3B. However, there are reasons for the gap. For example, if we could improve the result in 3B and find a $T_Q(k)$ bounded by a polynomial in k, then by theorem 4 we could simulate a nondeterministic $2^n$ time bounded machine deterministically in time $p(2^n)$ for some polynomial p. This is contrary to experience which indicates deterministic simulation of a nondeterministic $T(n)$ time bounded machine requires time $k^{T(n)}$ in general.

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

On the other hand, if we could push up the lower bound given in theorem 3A and show

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.

is unbounded, then we could conclude {Tautologies} $\notin \mathcal{L}^*$, since otherwise the general Herbrand proof procedure would provide a $T_Q(k)$ smaller than $2^k$. Thus such an improvement in 3A would require a major breakthrough in complexity theory.

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.

The field of mechanical theorem proving badly needs a basis for comparing and evaluating the dozens of procedures which appear in the literature. Performance of a procedure on examples by computer is a good criterion, but not sufficient (unless the procedure proves useful in some practical way). A theoretical complexity criterion is needed which will bring out fundamental limitations and suggest new goals to pursue.

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.)

The criterion suggested here (the function $T_Q(k)$) is probably too crude. For example, it might be better to make $T_Q(k)$ a function of several variables, of which one is $\phi(A)$, and another might be the minimum number of substitution instances of $fn(A)$ needed to form a contradiction (note that in general not all of $A_1, A_2, \ldots, A_{\phi(A)}$ are needed.)

$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ý.

$T_Q(k)$ may be a crude measure, but it does provide a basis for discussion, and, I hope, will stimulate progress toward finding better complexity measures for theorem provers.