Appendix

Organization The supplementary material is organized as follows: Section A presents a brief review of the concepts concerning first-order logic that are used in our work. Section C presents a proof of Theorem 1, our negative result concerning decision trees and OBDDs, while Section D is devoted to our positive result. Next, Section F presents a proof of Theorem 3, implying the full tractability of FOIL for a restricted class of OBDDs. Section G discusses details of the practical implementation, while Section H explains the the methodology of our experiments. Then, Section I discusses details of the high-level version we implemented, and also presents several examples of queries for the Student Performance Data Set which serve to show the usability of our implementation in practice. Finally Section J explains the binarization process for real-valued decision trees and high-level queries. We review the definition of first-order logic (FO) over vocabularies consisting only of relations. We assume the existence of a countably infinite set of variables {x, y, z,... }, possibly with subscripts. The set of FO-formulas over σ is inductively defined as follows. If x, y are variables, then x = y is an FO-formula over σ. 2. If relation symbol R σ has arity n > 0 and x If ϕ, ψ are FO-formulas over σ, then ( ϕ), (ϕ ψ), and (ϕ ψ) are FO-formulas over σ. 4. If x is a variable and ϕ is an FO-formula over σ, then ( x ϕ) and ( x ϕ) are FO-formulas over σ.