  The theory of definitional reflection (Hallnäs, 1991; Hallnäs, 2006; Hallnäs and Schroeder-Heister, 1990/91; Schroeder-Heister, 1993) takes up the challenge from logic programming and gives a proof-theoretic semantics not just for logical constants but for arbitrary expressions, for which a clausal definition can be given. Formally, this approach starts with a list of clauses which is the definition considered. Each clause has the form