Answer set programming in intuitionistic logic

As a demonstration of the flexibility of constructive mathematics, we propose an interpretation of propositional answer set programming (ASP) in terms of intuitionistic proof theory, in particular in terms of simply typed lambda calculus. While connections between ASP and intuitionistic logic are well-known, they usually take the form of characterizations of stable models with the help of some intuitionistic theories represented by specific classes of Kripke models. As such the known results are model-theoretic rather than proof-theoretic. In contrast, we offer an explanation of ASP using constructive proofs.