First-order answer set programming as constructive proof search

EasyChair Preprint 207

Abstract

We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the \Sigma_1 level of the Mints hierarchy in first-order intuitionistic logic. It follows that \Sigma_1 formulas using predicates of fixed arity (in particular unary) are of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation.

Keyphrases: Answer Set Programming, intuitionistic logic, lambda calculus, proof theory, stable model semantics

@booklet{EasyChair:207,
  author    = {Aleksy Schubert and Pawel Urzyczyn},
  title     = {First-order answer set programming as constructive proof search},
  doi       = {10.29007/9qvn},
  howpublished = {EasyChair Preprint 207},
  year      = {EasyChair, 2018}}