Reference. Finite-Choice Logic Programming

Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints—there is no single canonical model. The notion of stable models for logic programs with negation has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables. We propose a new formalism, finite-choice logic programming, that uses choice, not negation, to admit multiple solutions. Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain. We present an algorithm for exploring the solution space and prove it correct with respect to our semantics. Our implementation, the Dusa logic programming language, has performance that compares favorably with state-of-the-art answer set solvers and exhibits more predictable scaling with problem size.

Cite

Cite as @martens-2025-finite (helia, typst) · \cite{martens-2025-finite} (LaTeX)
BibTeX
bibtex · 1 line
@article{martens-2025-finite, title={Finite-Choice Logic Programming}, volume={9}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3704849}, DOI={10.1145/3704849}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Martens, Chris and Simmons, Robert J. and Arntzenius, Michael}, year={2025}, month=Jan, pages={362–390} }
hayagriva YAML (typst)
yaml · 19 lines
martens-2025-finite:
  type: article
  title: Finite-Choice Logic Programming
  author:
  - Martens, Chris
  - Simmons, Robert J.
  - Arntzenius, Michael
  date: 2025-01
  page-range: 362-390
  url: http://dx.doi.org/10.1145/3704849
  serial-number:
    doi: 10.1145/3704849
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 9
Cited by (1)

CounterChoice: Counterpoint Composition in Dusa with a Firmus Foundation erdem-2026-counterchoice

DOI
Cites 71 works (1 here)
With notes (1)

Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming dabral-2022-exploring

Informed consent has become increasingly salient for data privacy and its regulation. Entities from governments to for-profit companies have addressed concerns about data privacy with policies that enumerate the conditions for personal data storage and transfer. However, increased enumeration of and transparency in data privacy policies has not improved end-users’ comprehension of how their data might be used: not only are privacy policies written in legal language that users may struggle to understand, but elements of these policies may compose in such a way that the consequences of the policy are not immediately apparent. We present a framework that uses Answer Set Programming (ASP) – a type of logic programming – to formalize privacy policies. Privacy policies thus become constraints on a narrative planning space, allowing end-users to forward-simulate possible consequences of the policy in terms of actors having roles and taking actions in a domain. We demonstrate through the example of the Health Insurance Portability and Accountability Act (HIPAA) how to use the system in various ways, including asking questions about possibilities and identifying which clauses of the law are broken by a given sequence of events.
arXiv
External (70)
martens-2025-finite reference entries/refs/martens-2025-finite/martens-2025-finite.hel