Download PDFOpen PDF in browser

First-order answer set programming as constructive proof search

EasyChair Preprint no. 207

18 pagesDate: May 31, 2018

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:207,
  author = {Aleksy Schubert and Pawel Urzyczyn},
  title = {First-order answer set programming as constructive proof search},
  howpublished = {EasyChair Preprint no. 207},
  doi = {10.29007/9qvn},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser