λ. uniform proof
論理プログラミングの世界に uniform proof という概念があることを偶然知った。<URL:http://www.lix.polytechnique.fr/Labo/Dale.Miller/lolli/> の説明が分かりやすかったので以下に引用。
In order to determine whether a logic more expressive than Horn clauses (the logic of Prolog) could still be seen as the foundation of a logic programming language, Miller and Nadathur carefully analyzed the notion of goal-directedness and made the following definition. A proof is goal directed (or, in their words, uniform) if whenever a sequent has a non-atomic formula as its right hand side (that is, as the goal) then the rule used at that point is the one to decompose the goal. Logic programming, as distinct from theorem proving, can be seen as the search for uniform proofs. A logic is appropriate as a foundation of a logic programming language if uniform proofs are complete for that logic.