Learning Programs as Logical Queries
Type 1 Paper

Charles Jordan1? and Lukasz Kaiser2
1

ERATO Minato Project, JST & Hokkaido University
2
LIAFA, CNRS & Université Paris Diderot
skip@ist.hokudai.ac.jp, kaiser@liafa.univ-paris-diderot.fr

Abstract. Program learning focuses on the automatic generation ofprograms satisfying the goal of a teacher. One common approach iscounter-example guided inductive synthesis, where we generate a sequenceof candidate programs and the teacher responds with counter-examples
for which the candidate fails. In this paper we focus on a logical approach,where programs are tuples of logical formulas, i.e. logical queries, andinputs and outputs are relational structures. We introduce our modelof inductive synthesis and our implementation of it using SAT and
QBF solvers. We survey basic theoretical properties of our model andshow a few experimental results: learning complexity-theoretic reductions,polynomial-time programs, and learning board games from examples.

1

Introduction

The dream of program learning – that instead of writing code we will teachcomputers to derive it automatically – has a long history in computer scienceand has appeared in many forms. In program synthesis we seek any programthat satisfies a specification, usually given as a logical formula. However, writing
this formal logical specification can be as hard as writing the program itself. To
avoid formal specifications, one can consider learning programs using only a setof example inputs and outputs.
Program learning is difficult and there are many theoretical and practicalchallenges. Specifying the exact requirements for the learner is already hard. One
must choose a representation of programs, what assumptions on efficiency tomake, whether the goal is any program or a short one, and the precise meaning of“short”. More practically, searching for programs in any standard programming
language is very inefficient. Most problems are undecidable, there are hardly any
useful normal forms to exploit, and modifying even a small part of a program
can dramatically change its behavior. Given these issues, it is easy to understand
why the dream of program learning has not yet been realized.
Choosing a representation for programs is critical and recent work [1,8,9] indescriptive complexity suggests that logical queries are uniquely suited for thistask. Descriptive complexity studies the connection between logics and complexity?

This work was supported in part by KAKENHI Grant Number 25106501.

classes: logics equivalent to classes such as NL, P, NP, and PSPACE are known.
Searching for formulas in these logics corresponds to searching for programs inthese classes, and has other advantages that we discuss below.
Here, we introduce a model of learning programs represented by logical queries.
Our approach tries to address the theoretical challenges with program learning
mentioned above, and we leverage recent advances in SAT and QBF solvers
to address more practical concerns. We have implemented our model3 and we
describe three kinds of initial experiments. For program synthesis, we describe
learning complexity-theoretic reductions and also polynomial-time equivalents
for NP programs. Both of these tasks have complete specifications. To show that
this is not a limitation of our approach, we experiment with learning the rules ofboard games from sets of example plays. While these experiments are preliminary,
we believe the results show that our approach to program learning is promising.
Related Work. Much of our motivation comes from recent papers using ideas fromdescriptive complexity in inductive synthesis. For example, given a specificationin an expressive logic (second-order), [8] synthesized equivalent formulas inless expressive logics which can be evaluated more efficiently. Automaticallyfinding complexity-theoretic reductions between computational problems was
first considered by [1]. They focused on quantifier-free reductions, a weak classof reduction defined by tuples of quantifier-free formulas.
Both problems are essentially the same – finding formulas in a particular form
that satisfy desired properties. However, the implementations are separate andnot publicly available. We [9] have previously compared a number of different
approaches to reduction finding. In this paper, we introduce a more generalapproach – allowing the user to specify an “outline” of the desired formula and a
specification that it must satisfy. We provide a single model and freely available
implementation that can be used to experiment with various synthesis problems.
Inductive synthesis has a long history and there is a tremendous amount ofwork that we do not cover here. See, e.g., [4,11] for a more general perspective.

2

Background in Logic and Descriptive Complexity

In this section we briefly review the necessary background from descriptive
complexity. For more details, see [7] or Chapter 3 of [3].
There are many possible representations of programs; in this paper, we focus
on logical representations. One benefit of the logical approach is that we areable to treat structures such as graphs directly, instead of encoding them intowords or numbers. This allows us to express many interesting programs succintly,
and formulas have natural normal forms. These provide guidance for hypothesis
spaces, and improve understandability of learned programs.
Fundamentally, programs transform given inputs into outputs; we represent
these inputs and outputs as relational structures (for example, graphs or binary
strings). A relational signature is a tuple of predicate symbols Ri with arities ai
3

All source code is freely available in the 0.9 release of Toss at http://toss.sf.net.

2and constant symbols cj , τ := (R1a1 , . . . , Rrar , c1 , . . . , cs ). A finite τ -structure
consists of a finite universe U , an ai -ary relation for each predicate symbol of τ ,and a definition – an element of U – for each constant symbol:
A := (U, R1 ⊆ U a1 , . . . , Rr ⊆ U ar , c1 ∈ U, . . . , cs ∈ U ) .
For example, the signature for directed graphs contains a single, binary predicate
symbol E and so a directed graph consists of a finite set of vertices and abinary edge relation. We denote the set of all finite τ -structures by Struc(τ ). Our
programs are built from formulas in various logics. Formulas of first-order logic
over a signature τ have the form
ϕ := Ri (x1 , . . . , xai ) | xi = xj | xi = cj | ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ∃xi ϕ | ∀xi ϕ,where x1 , x2 , . . . are first-order variables, and the semantics, given an assignmentof the variables xi to elements ei of the structure, is defined in the natural way.
Queries. Single formulas can be used to define properties or decision problems,
but in general we represent programs as queries. Queries map σ-structures toτ -structures, defining the universe, relations, and constants using logical formulas.
A first-order query from σ-structures to τ -structures is an r + s + 2-tuple,
q := (k, ϕ0 , ϕ1 , . . . , ϕr , ψ1 , . . . , ψs ) .
The number k ∈ N is the dimension of the query. Each ϕi , ψj is a first-orderformula over the signature σ. Let A be a σ-structure with universe U A . The
formula ϕ0 has free variables x1 , . . . , xk and defines the universe U of q(A),U := (u1 , . . . , uk ) | ui ∈ U A , A |= ϕ0 (u1 , . . . , uk ) .
That is, the new universe consists of k-tuples of elements of the old universe,
where ϕ0 determines which k-tuples are included.
Each remaining ϕi has free variables x11 , . . . , xk1 , x12 , . . . , xkai and definesRi := (u11 , . . . , uk1 ), . . . , (u1ai , . . . , ukai ) | A |= ϕi (u11 , . . . , ukai ) ∩ U ai .
That is, ϕi determines which of the ai -tuples of U are included in Ri . Finally,each ψi has free variables x1 , . . . , xk and defines ci as the unique (u1 , . . . , uk ) ∈ Usuch that A |= ψi (u1 , . . . , uk ).
First-order queries therefore transform σ-structures into τ -structures, and wewrite q(A) to represent the resulting τ -structure. The restriction to first-orderlogic here is not essential – given a logic L, we define L-queries in a similar way.
Extending first-order logic. So far, we have focused only on first-order logic.
However, first-order logic on finite structures is often too limited from thecomputational perspective – it cannot express many interesting queries that areeasy to compute. Over finite structures with additional numeric predicates, thefirst-order definable properties correspond exactly to uniform AC0 (cf. [7]).
To remove this limitation, one extends first-order logic with various operators.
For example, the transitive closure operator allows us to write formulas of the3form TC[x1 , x2 .ϕ(x1 , x2 )](y1 , y2 ). This formula takes the transitive and reflexive
closure of the (implicit) relation defined by ϕ(x1 , x2 ) and evaluates it on (y1 , y2 ).
The least fixed-point operator allows recursive definitions in formulas of the form
LFP[R(x1 , . . . , xk ) = ϕ(R, x1 , . . . , xk )](y1 , . . . , yk ), where R is a new relation
symbol appearing only positively in the inner formula ϕ. The result of thisoperator is defined as the least fixed-point of the operator R(x) → ϕ(R, x).
Finally, second-order logic (SO) allows to use quantifiers over relations.
There are many known correspondences between logics and complexity classses(see [7]). The oldest result [2] shows that the class NP is captured by existential
second-order logic. This implies that coNP is captured by universal second-orderlogic, and that full SO captures the polynomial-time hierarchy. More practically,polynomial-time computations are captured by least fixed-point logic (LFP)
when a linear order relation is present [5,12]. Although LFP is presumably more
expressive than transitive closure logic (TC), TC captures all problems solvablein non-deterministic logarithmic space (NL) on ordered structures [6].
Outlines. For a logic L, we refer to the set of L-formulas in which atoms a may be
guarded by some Boolean guard4 Ga as L-formula outlines. The Boolean guards
are intended to mean “a occurs here”, and given an instantiation of the guards I,
we can instantiate an L-formula outline ψ to an L-formula ψ I by replacing each
Ga a by a if Ga is true in I, and leaving the atom empty otherwise. Intuitively,
an outline fixes the structure of the formula but not the precise contents. We
refer to queries containing L-formula outlines as L-query outlines. We omit L
when it is clear from context, and use outline to refer to both query and formula
outlines. Given an outline o, we write inst(o) for the set of formulas or queries
obtainable as instantiations of o.

3

Learning Logical Queries

In this section, we introduce our model of learning logical queries. The model
consists of a learner giving candidate queries or hypotheses and a teacher (orverifier), which gives counter-examples or accepts the query. A learning task ischaracterized by a few parameters, first is the target class C.
Let C ⊆ Struc(τ ) × Struc(σ) be a binary relation on relational structures, anddefine the domain of C as dom(C) = {A | (A, B) ∈ C for some B}.
Definition 1. A C-teacher t is a functiont : (τ → σ)-queries → (dom(C) × SO(σ)) ∪ {⊥}that satisfies the following condition.
(⊥
if {(A, q(A)) | A ∈ dom(C)} ⊆ C,
t(q) =(A, ψ) where A ∈ dom(C), (A, q(A)) 6∈ C, (B |= ψ iff (A, B) ∈ C) .
4

We do not require that identical atoms share guards, that distinct atoms have different
guards, or that all atoms are guarded.

4

That is, a teacher accepts a query q if for all A ∈ dom(C) we have (A, q(A)) ∈ C,
and otherwise replies with a counter-example (A, ψ) such that q(A) 6|= ψ. Here,the formula ψ defines the acceptable output on A. Of course, in practice wegenerally restrict attention to computable teachers and “reasonable” classes C.
Definition 2. Let H be a class of logical queries. An H-learner L is a function
that, given a sequence of examples ((A1 , ψ1 ), . . . , (Am , ψm )), satisfies(
h, h ∈ H, h(Ai ) |= ψi for 1 ≤ i ≤ m;
L((A1 , ψ1 ), . . . , (Am , ψm )) =⊥, if no such h ∈ H exists .
Note that our learners must always be consistent, and they return ⊥ iff there
is no consistent query in the hypothesis space. The logic used in the query isdetermined by H. In practice, we always use outline learners, which are definedas H-learners for H = inst(q) for some query outline q.
The outline gives a compact representation of a hypothesis space, and can also
enforce certain restrictions on the query. For example, outlines can require a queryto generate an extension 5 of the structure, which is useful when searching for
programs to give explicit isomorphisms or satisfying solutions to SAT instances.
Outline learners using QBF solvers. Essentially, an outline learner is a learnerwith a finite, uniform
hypothesis space. The main condition of an outline learner,
Vnamely that i q I (Ai ) |= ψi , can be translated into a QBF formula. This isdone by introducing a Boolean variable for each tuple in each relation in q I (Ai ),setting it to true only if the respective formula from q holds for the specified
tuple, and then translating ψi using these Boolean variables for relations. We
omit the complete algorithm due to space constraints, but it is crucial that all
logics we consider are expressible in SO and that each ψi ∈ SO, by the definitionof a teacher. This allows us to implement outline learners using QBF solvers tosearch for a suitable instantiation of the guards. For a query outline q and a QBF
solver S, we write L(S, q) for the inst(q)-learner using S as explained above.
Given an H-learner L and a C-teacher t we define the sequence Lti of theinteractions between L and t inductively as follows. We set Lt0 := L(), thehypothesis that L returns on an empty list of examples. If for some i we get
Lti = ⊥ then the sequence is finished – there is no h ∈ H that satisfies theteacher. Else, let Ei := t(Lti ) be the answer of the teacher to Lti . If Ei = ⊥ thesequence Lti is finished, the last hypothesis was accepted. In the other case, set
Lti+1 = L(E0 , . . . , Ei ). The following properties are immediate.
Theorem 3. Let S be a correct QBF solver, t a C-teacher, and q a query outline.
1. L(S, q) is a consistent and conservative inst(q)-learner.
2. If t(h) = ⊥ for some h ∈ inst(q) then the sequence L(S, q)ti is finite and its
last element g satisfies t(g) = ⊥.
3. If there is no h ∈ inst(q) for which t(h) = ⊥ then the sequence L(S, q)ti isfinite and its last element is ⊥.
5

An extension of a structure is formed by adding new predicates while leaving existing
predicates unchanged.

5

Of course, we often have to restrict the teacher in order to obtain decidability.
We usually restrict C to be a finite set, and usually implement the teacher using
SAT or QBF solvers as well6 . Although one can easily construct instances where
arbitrarily-large examples are required, in practice it seems that queries that are
correct on moderately sized examples are almost always correct in general (where“moderate” depends on the complexity of the query).
A learning task is specified by the pair (C, H). We write L(t, q) for the lastelement of the sequence L(S, q)ti , where S is a chosen solver. The sequence isalways finite by Theorem 3, so L(t, q) is well-defined. In the next section, we
examine various learning tasks and look for reasonable teachers and outlines.

4

Experimental Results

4.1

Learning Reductions

Learning reductions was first considered by [1], and we have also [9] implemented,
benchmarked and evaluated a number of different approaches to the problem.
Problem. In descriptive complexity, a reduction from the τ -property defined by
ϕ to the σ-property defined by ψ is a (τ → σ)-query q that satisfies
A |= ϕ ⇐⇒ q(A) |= ψ(1)for all τ -structures A. Of course, reductions should have less computational power
than the complexity classes they are used in and descriptive complexity focuses
on first-order reductions (i.e., first-order queries as reductions). Here, we focus on
quantifier-free first-order reductions, a weaker class that still suffices to capture
important complexity classes (cf. [9] for more details).
In order to make finding quantifier-free reductions decidable, we restrict
attention to a fixed size n, i.e., we require Formula (1) to hold only for structuresof size at most n. Assume that we are searching for a dimension-k reduction fromthe τ -property defined by ϕ to the σ-property defined by ψ.
Let P be the set of τ -structures of size at most n that satisfy ϕ, Q be the set ofσ-structures of size at most nk that satisfy ψ, and P and Q be their complements
up to the size bounds. Our target class is C = (P × Q) ∪ (P × Q) – we want aquery that maps positive instances to positive instances and negative instances
to negative instances.
Outline. As an outline, we focus on reductions in which all formulas are in DNF
with c conjunctions. We fix ϕ0 to be always true and the dimension k (so the
new universe is the set of k-tuples of elements of the old universe). Finally, we
have a number of parameters determining the atomic formulas that may occur –for example, whether to allow certain numeric predicates such as successor.
6

We recommend GlueMiniSat as a SAT and RAReQS as a QBF solver, c.f. [9].

6Teacher. When the teacher receives a candidate hypothesis q, it checks Formula (1), i.e. A |= ϕ ⇐⇒ q(A) |= ψ for all structures A of size at most n. Thisis done by assigning a Boolean variable to each bit of A and q(A), and thenconstructing a QBF (or SAT) instance similar to the learner L(S, q) describedabove. If the instance is satisfied, the assignment returned by the solver is used
to construct a structure A that is a counter-example to the hypothesis q. The
teacher returns (A, ψ) if A |= ϕ and (A, ¬ψ) otherwise.
Results. We refer to [9] for more details on our reduction-finding experiments. Our
approach using GlueMiniSat as solver significantly improves upon the previous,
specialized program ReductionFinder [1].
Example. Consider the NL-complete problems of reachability (given a directed
graph with labeled vertices s and t, determine whether t is reachable from s) andall-pairs reachability (determine if a directed graph is strongly connected).
Reach := T C[x, y.E(x, y)](s, t)

AllReach := ∀x1 , x2 (T C[y, z.E(y, z)](x1 , x2 )) .

Our system finds the following correct reduction for n ≥ 3 in less than a second:(k := 1, ϕ0 := true, ϕ1 := x1 = s ∨ x2 = t ∨ E(x2 , x1 )) .
This reverses all edges in the original graph, adds directed edges from s to all
vertices and also adds directed edges to t from all vertices. A similar reduction
exists without reversing the edges – however the above is our actual output.

4.2

Learning Fast Programs

In this section, we consider synthesizing programs for a given logical specification.
This is similar to [8], however they focused on synthesizing formulas in more
specialized logics.
Problem. In program synthesis, we are given a specification and hope to find an
efficient program satisfying it. For us, a specification is a way to verify whether
the output q(A) is accepted for A. There are two major variations – either the
output for each structure is unique (as in our example here), or there is a set of
acceptable outputs (e.g., when finding a satisfying solution for SAT instances).
In our example here, we have a query s in an expressive logic (SO) and wish
to find an equivalent query in a less-expressive logic. In particular, we consider
the problem of identifying winning regions in finite games – i.e., directed graphswith a predicate V0 (x) meaning that vertex x belongs to Player 0. Decidability
requires restricting the size of the games n, and we set C to be the set of pairs(A, B) such that A is a finite game of size at most n and B is the extension of A
with the winning region identified in a new monadic predicate W .
7Outline. Similar to the case for reductions, we use several parameters to fix anoutline. For reductions, we considered only quantifier-free formulas – however,in this section we need more expressive power. We focus on least fixed-point
formulas, with a single fixed-point operator that is outermost7 . We fix the arity aof the fixed-point predicate, and assume that the inner formula is a disjunctionof l quantified CNF formulas with k variables each. We use such an outline forexactly one selected relation W in the query, all others are set to identity.
Teacher. Assume that we have a SO query s that produces the desired extension
with the winning region identified. Given a hypothesis q, the teacher can again
use a SAT or QBF solver (as was the case for reductions) to guess a game A ofsize at most n such that in q(A) the new relation W (x) is not equivalent to theregion in s(A). Let a1 , . . . , ak be thein s(A). The teacher then
W winning positions
returns the pair A, ∀x (W (x) ↔ i (x = ai )) .
Example. Consider the case of identifying winning regions in finite reachability
games. When the current vertex belongs to a player, that player chooses anoutgoing edge and moves to a connected vertex. Player 1 loses if the play reaches
a vertex that belongs to her and has no outgoing edge. Similarly, Player 0 loses if
the play reaches a position where he must but cannot move, but also if the play
becomes a cycle and goes on forever. The goal is to identify the vertices fromwhich Player 0 has a winning strategy. That is, we want a formula ϕ(x) whichholds exactly on the vertices for which Player 0 has a winning strategy.
Reachability games are positional, i.e., it suffices to consider strategies that
depend only on the current position and not on the history of the game. Therefore,
a strategy of Player 1 can be defined as a binary relation S1 that is a subset ofthe edges and that, for vertices of Player 0, contains all successors of the vertex
as well. Then, x is winning for Player 1 (by S1 ) if all vertices reachable from x
by S1 either belong to Player 0 or have an S1 -successor. This is easily expressibleusing the TC operator and guessing the strategy leads to a second-order formula
ϕ0 (x) which holds exactly if x is winning for Player 0.
In reachability games, the following LFP formula defines the winning region
for Player 0:hn
LFP W (x) = (¬∃x1 : (¬W (x1 ) ∧ E(x, x1 )) ∧ ¬V0 (x)) ∨oi∃x1 : (W (x1 ) ∧ E(x, x1 ) ∧ V0 (x)) (x) .
The LFP operator recursively defines W (x), starting with the empty set andadding tuples that satisfy the formula on the right until a fixed-point is reached.
Therefore, this formula says that a position x is winning for Player 0 if(a) it is the opponent’s move and all outgoing edges go to positions we win; or(b) it is Player 0’s move and there is an edge to a winning position.
Recall that the fixed-point predicate is initially empty. Therefore, the winning
positions after one iteration are the positions belonging to the opponent with no7

This is a normal-form for fixed-point logics, although the arity of the fixed point may
increase if it is required to be outermost.

8

outgoing edges. Then, the winning region grows gradually until it is the attractorof those positions – which is correct. An equivalent, slightly longer formula isfound by our program in less than a minute for n ≥ 3.
Further work. The LFP formula for reachability games can be written by hand,but our motivation for presenting this example is the hope to compute polynomialtime solvers for other games. In particular, weak parity games and parity games
are also positional, so it is trivial to write a SO formula defining the winning
region (as we did for reachability games). But the polynomial-time program forsolving weak parity games is complicated, and the existence of a polynomial-time
solver for full parity games (which is equivalent to the existence of an LFP
formula) is a long-standing open problem.
Our implementation can also search for other programs, for example, programsfor graph isomorphism, graph coloring or SAT. There are natural classes wherethese problems are in polynomial-time8 .
4.3

Learning Formulas from Examples

Recently, a system was implemented [10] that represents board games as relational structures and learns their rules from observing example play videos.
Fundamentally, the system works by computing minimal distinguishing formulas
for sets of structures, e.g., formulas satisfied by structures representing winning
positions and by none of the losing ones. We implement the computation of
distinguishing formulas in our framework and compare the performance.
Problem. Let P and N be finite sets of τ -structures. We want to learn a formula
ϕ without free variables such that A |= ϕ for all A ∈ P and for no A ∈ N . Unlike
previous tasks, we want a minimal such formula, not just an arbitrary one.
Outline and Teacher. We use the same outlines as for the program synthesistask. However, we focus on first-order formulas, i.e., we set a = 0. Moreover, tofind minimal formulas we iterate through k, and for each k we range l from 1 tok + 1. The teacher is simple: given a formula ϕ it checks if A |= ϕ for all A ∈ P,
and if not, it returns (A, true) for some A 6|= ϕ. Then, it checks if A 6|= ϕ for all
A ∈ N and returns (A, false)9 if this is not the case for some A |= ϕ.
Results. We substituted our SAT-based learner for the procedure for computing
distinguishing formulas used in [10]. Comparing the results, the SAT-based
approach appears to offer significantly better performance.

Original system
SAT-based system

Breakthrough Connect4 Gomoku Pawn-Whopping
113s
33s
11s
936s
5s
16s
5s
131s

8

E.g., isomorphism of planar graphs, bounded-degree graphs, and graphs excluding aminor; k-SAT and k-coloring are NL-complete for k = 2 and NP-complete for k ≥ 3.
9Here, “true” and “false” are satisfied by encoded Boolean structures.

9

We use the same example plays for both systems – these examples were chosen
by hand for the original system in [10]. But our SAT-based approach searches(faster) for formulas in more expressive logics, beyond reach for the original
system. For this reason, the resulting formulas are not always correct – they are
for Breakthrough and Gomoku, but not for Connect4 and Pawn-Whopping. It
would be easy to overcome this by adding examples or changing the outline tomatch the more restrictive logics used by the original system.

5

Conclusions and Future Work

Thanks to the efficiency of modern SAT and QBF solvers, our general procedure
outperforms specialized programs both in learning reductions [1] and in learningfrom examples [10]. We consider these early results promising and encourage
further experimentation with our freely available implementation.
There are many questions we leave unanswered. For example, there is a large
variance in runtime depending on the precise series of counter-examples givenby the teacher. We would like to know how to choose “good” counter-examples
and whether randomness [13] can help. We ask what outlines are “good”, how tochoose them to find the desired programs quickly and to make them readable.
We are interested in re-using sub-formulas found for one problem to speed up
learning in another one, and in extending our approach to quantitative settings.

References
1. Crouch, M., Immerman, N., Moss, J.E.B.: Finding reductions automatically. In:
Fields of Logic and Computation. LNCS, vol. 6300, pp. 181–200 (2010)
2. Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets.
In: Complexity of Computation, SIAM-AMS Proceedings. vol. 7, pp. 43–73 (1974)
3. Grädel, E., Kolaitis, P.G., Libkin, L., Marx, M., Spencer, J., Vardi, M.Y., Venema,Y., Weinstein, S.: Finite Model Theory and Its Applications. Springer (2007)
4. Gulwani, S.: Dimensions in program synthesis. In: Proc. PPDP 2010. pp. 13–24.
New York, NY, USA (2010)
5. Immerman, N.: Relational queries computable in polynomial time. In: Proc.
STOC’82. pp. 147–152 (1982)
6. Immerman, N.: Languages that capture complexity classes. SIAM J. Comput. 16(4),760–778 (1987)
7. Immerman, N.: Descriptive Complexity. Springer-Verlag (1999)
8. Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis
methodology and its applications. In: Proc. OOPSLA’10. pp. 36–46 (2010)
9. Jordan, C., Kaiser, L.: Experiments with reduction finding. In: Proc. SAT 2013
10. Kaiser, L.: Learning games from videos guided by descriptive complexity. In: Proc.
AAAI 2012. pp. 963–970 (2012)
11. Kitzelmann, E.: Inductive programming: A survey of program synthesis techniques.
In: AAIP 2009, Revised Papers. LNCS, vol. 5812, pp. 50–73 (2010)
12. Vardi, M.Y.: The complexity of relational query languages. In: Proc. STOC’82. pp.
137–146 (1982)
13. Zeugmann, T.: From learning in the limit to stochastic finite learning. Theoret.
Comput. Sci. 364(1), 77–97 (2006)10