Proving failure in functional logic programs (extended version

Abstract. How to extract negative information from programs is an important issue in logic programming. Here we address the problem for functional logic programs, from a proof-theoretic perspective. The start-ing point of our work is CRWL (Constructor based ReWriting Logic), a well established theoretical framework for functional logic program-ming, whose fundamental notion is that of non-strict non-deterministic function. We present a proof calculus, CRWLF, which is able to deduce negative information from CRWL-programs. In particular, CRWLF is able to prove ‘ nite ’ failure of reduction within CRWL.