 after iterating through all possible y's e will become true. □ Before we turn to prove Thm. 6.2 and establish a lower bound on the query complexity in the Hoare model, we note that this construction also yields the computational hardness mentioned in §4: Proof of Thm. 4.2. The upper bound is straightforward: guess an invariant in CNF p(n) and check it. For the lower bound, use the reduction outlined above: given ϕ(y 1,..., y k, x 1,..., x k ), construct TS ϕ. Note that the vocabulary size, n, is 2k + 3, and the invariant, when exists, is of length at most 2k + 1 ≤ n. 8 The reduction is polynomial as the construction of TS ϕ (and n) from ϕ is polynomial in k and |ϕ |: note that lexicographic incrementation can be performed with a propositional formula of polynomial size. □ 6.1.2 Lower Bound's Proof. We now turn to prove Thm. 6.2. Given an algorithm with polynomial query complexity, the proof constructs two transition system: one that has a polynomial-length invariant and one that does not, and yet all the queries the algorithm performs do not distinguish between them. The construction uses the path the algorithm takes when all Hoare queries return false as much as possible. Intuitively, such responses are less informative and rule out less transition relations, because they merely indicate the existence of a single counterexample to a Hoare triple, opposed to the result true which indicates that all transitions satisfy a property.
Proof of Thm. 6.2. Let A be a computationally unbounded Hoare-query algorithm. We show that the number of Hoare queries performed by A on transition systems from P Σ P 2 with |Σ| = n is at least 2 n−1 2. To this end, we show that if A over |Σ| = 2n + 3 performs less than 2 n queries, then there exist two formulas ψ 1,ψ 2 over y 1,..., y n, x 1,..., x n such that • all the Hoare queries performed by A on δ P ψ 1 and δ P ψ 2 (the transition relations of TS ψ 1 and TS ψ 2, respectively) return the same result, even though • A should return different results when run on TS ψ 1 ∈ P n Σ P 2 and TS ψ 2 ∈ P n Σ P 2, since TS ψ 1 has an invariant in Mon-CNF 2n+1 and TS ψ 2 does not have an invariant (of any length). We begin with some notation. Running on input TS ϕ, we abbreviate H (δ P ϕ, ·, ·) by H (ϕ, ·, ·). Denote the queries A performs and their results by H (ϕ, α 1, β 1 ) = b 1,..., H (ϕ, α m, β m ) = b m. We call an index i sat if b i = false. We say that ψ query-agrees with ϕ if H (ψ, α i, β i ) = b i for all i. We say that ψ sat-query-agrees with ϕ if for every i such that b i = false it holds that H (ψ, α i, β i ) = false.
We first find a formula ϕ over y 1,..., y n, x 1,..., x n such that the sequence of queries A performs when executing on TS ϕ is maximally satisfiable: if ψ sat-query-agrees with ϕ, then ψ (completely) query-agrees with ϕ on the queries, that is, We construct this sequence iteratively (and define ϕ accordingly) by always taking ϕ so that the result of the next query is false as long as this is possible while remaining consistent with the results of the previous queries: Initially, choose some arbitrary ϕ 0. At each point i, consider the first i queries A performs on ϕ i, H (ϕ i, α 1, β 1 ) = b 1,..., H (ϕ i, α i, β i ) = b i. If A terminates without performing another query, we are done: the desired ϕ is ϕ i. Otherwise let (α i+1, β i+1 ) be the next query. Amongst formulas ϕ i+1 that query-agree on the first i queries, namely, H (ϕ i+1, α j, β j ) = b j for all j ≤ i, choose one such that H (ϕ i+1, α i+1, β i+1 ) = false if possible; if such ϕ i+1 does not exist take e.g. ϕ i+1 = ϕ i. The dependency of A on ϕ i is solely through the results of the queries to H (δ P ϕ, ·, ·), so A performs the same i initial queries when given ϕ i+1. The result is a maximally satisfiable sequence, for if a formula ψ differs in query i + 1 in which the result is false instead of true we would have taken such a ψ as ϕ i+1.
Let ϕ be such a formula with a maximally satisfiable sequence of queries A performs on ϕ, of δ P ϕ depends on the value of ϕ on at most one assignment to x, y, so there exists a valuation v i : y ∪ x → {true, false} such that as well. It follows that Let v i 1,..., v i t be the valuations derived from the sat queries (concerning indexing, b i = false iff b i = b i j for some j). We say that a formula ψ valuation-agrees with ϕ on for all j's. Since the sequence of queries is maximally satisfiable, if ψ valuation-agrees with ϕ on v i 1,..., v i t then ψ query-agrees with ϕ, namely, H (ψ, α i, β i ) = H (ϕ, α i, β i ) for all i = 1,..., m. As the dependency of A on ϕ is solely through the results b 1,..., b m, it follows that A performs the same queries on ψ as it does on ϕ and returns the same answer.
It remains to argue that if m < 2 n then there exist two formulas ψ 1,ψ 2 that valuation-agree with ϕ on v i 1,..., v i t but differ in the correct result A should return: ∃y. ∀x. ψ 1 (y, x) is true, and so TS ψ 1 has an invariant in Mon-CNF 2n+1 (Lemma 6.3), whereas ∃y. ∀x. ψ 2 (y, x) is not, and so TS ψ 2 does not have an invariant of any length or form (Lemma 6.3). This is possible because the number of constraints imposed by valuation-agreeing with ϕ on v i 1,..., v i t is less than the number of possible valuations of x for every valuation of y and vice versa: is true on all valuations except for some of v i 1,..., v i t, and since t ≤ m < 2 n there exists some y such that for all x, (y, x) is not one of these valuations (recall that |y| = n bits). Dually, is false on all valuations except for some of v i 1,..., v i t, and since t ≤ m < 2 n for every y there exists x such that (y, x) is not one of these valuations (recall that |y| = n bits). This concludes the proof. □
An algorithm in the interpolation-query model, also called an interpolation-query algorithm, is an inference from queries algorithm expecting any interpolation query oracle, where k 1, k 2 are bounded by a polynomial in n in all queries. The query complexity in this model is q itp A (n).
Interpolation-query oracles form a family of oracles since different oracles can choose different ρ for every δ, α, β, k 1, k 2. Note that ρ may be exponentially long.

Lower Bound on Interpolation-Query Algorithms.
We show an exponential lower bound on query complexity for interpolation-query algorithms. To this end we prove the following adaptation of Thm. 6.2: Theorem 6.6. Every interpolation-query inference algorithm, even computationally-unrestricted, deciding polynomial-length inference for the class of transition systems P Σ P 2 ( §6.1.1) has query complexity of 2 Ω(n).
We remark that the lower bound on the interpolation-query model does not follow directly from the result for the Hoare-query model: an interpolant for H (k 1 +k 2 ) (δ, α, β) = true depends on all traces of length k 1 + k 2 starting from states satisfying α, which may be an exponential number, so it cannot be computed simply by performing a polynomial number of Hoare queries to find these traces and computing an interpolant based on them. In principle, then, an interpolant can convey information beyond a polynomial number of Hoare queries. Our proof argument is therefore more subtle: we show that there exists