First-order Answer Set Programming as Constructive Proof Search

DOI10.1017/S147106841800008XMaRDI QIDQ4559822zbMATH OpenOpenAlexFDO

Authors Aleksy Schubert, Paweł Urzyczyn

Publication date 4 December 2018

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1804.10004

zbMATH Keywords

answer set programmingintuitionistic logiclambda calculusproof terms

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Logic programming (68N17)

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) is 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. This paper is under consideration for publication in Theory and Practice of Logic Programming

Recommendations

• scientific article; zbMATH DE number 6536279
• Answer set programming based on propositional satisfiability
• scientific article; zbMATH DE number 4170865
• Preferred first-order answer set programs
• scientific article; zbMATH DE number 1882048
• Answer Set Programming: A Declarative Approach to Solving Search Problems
• scientific article; zbMATH DE number 1113998
• Answer set programming in intuitionistic logic
• On structuring proof search for first order linear logic
• On structuring proof search for first order linear logic

Cites work

• Answer set programming in intuitionistic logic
• Applications of intuitionistic logic in Answer Set Programming
• Autoepistemic logic
• Equilibrium logic
• On the Mints hierarchy in first-order intuitionistic logic
• Operational semantics of resolution and productivity in Horn clause logic
• Restricted positive quantification is not elementary
• Stable inference as intuitionistic validity

Cited in

(5)

• A progression semantics for first-order logic programs
• Connecting first-order ASP and the logic FO(ID) through reducts
• scientific article; zbMATH DE number 6536279 (Why is no real title available?)
• The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
• A Survey of the Proof-Theoretic Foundations of Logic Programming

This page was built for publication: First-order Answer Set Programming as Constructive Proof Search

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4559822)