First-order Answer Set Programming as Constructive Proof Search

DOI10.1017/S147106841800008XzbMath1451.68067arXiv1804.10004OpenAlexW2963528460MaRDI QIDQ4559822

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

intuitionistic logiclambda calculusanswer set programmingproof terms

Mathematics Subject Classification ID

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

Related Items (2)

A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

Cites Work

• Equilibrium logic
• Answer set programming in intuitionistic logic
• Operational semantics of resolution and productivity in Horn clause logic
• Stable inference as intuitionistic validity
• Autoepistemic logic
• Applications of intuitionistic logic in Answer Set Programming
• Restricted Positive Quantification Is Not Elementary
• On the Mints Hierarchy in First-Order Intuitionistic Logic

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