Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Relating Answer Set Programming and Many-sorted Logics for Formal Verification

Zachary Hansen

TL;DR

This work argues that formal verification of Answer Set Programming (ASP) can be made routine by translating ASP into here-and-there (HT) and many-sorted first-order logic, enabling modular reasoning and automated theorem-prover verification. It surveys foundational translations (Clark's Completion, loop formulas) and advances in HTA-based formalisms, introducing SM-based minimization and modular proofs. The author reports progress on conditional literals and aggregate semantics, extends mini-gringo and anthem with new features, and develops program-to-program verification (AP2P) and Anthem 2, demonstrating practical verification workflows. Ongoing work targets recursive aggregates, deeper integration of sets with many-sorted logic, and broader tooling and interoperability to promote practice-oriented formal verification in ASP.

Abstract

Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy (especially, artificially intelligent) software systems. However, formally verifying ASP programs offers some unique challenges, such as 1. a lack of modularity (the meanings of rules are difficult to define in isolation from the enclosing program), 2. the ground-and-solve semantics (the meanings of rules are dependent on the input data with which the program is grounded), and 3. limitations of existing tools. My research agenda has been focused on addressing these three issues with the intention of making ASP verification an accessible, routine task that is regularly performed alongside program development. In this vein, I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic. These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.

Relating Answer Set Programming and Many-sorted Logics for Formal Verification

TL;DR

This work argues that formal verification of Answer Set Programming (ASP) can be made routine by translating ASP into here-and-there (HT) and many-sorted first-order logic, enabling modular reasoning and automated theorem-prover verification. It surveys foundational translations (Clark's Completion, loop formulas) and advances in HTA-based formalisms, introducing SM-based minimization and modular proofs. The author reports progress on conditional literals and aggregate semantics, extends mini-gringo and anthem with new features, and develops program-to-program verification (AP2P) and Anthem 2, demonstrating practical verification workflows. Ongoing work targets recursive aggregates, deeper integration of sets with many-sorted logic, and broader tooling and interoperability to promote practice-oriented formal verification in ASP.

Abstract

Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy (especially, artificially intelligent) software systems. However, formally verifying ASP programs offers some unique challenges, such as 1. a lack of modularity (the meanings of rules are difficult to define in isolation from the enclosing program), 2. the ground-and-solve semantics (the meanings of rules are dependent on the input data with which the program is grounded), and 3. limitations of existing tools. My research agenda has been focused on addressing these three issues with the intention of making ASP verification an accessible, routine task that is regularly performed alongside program development. In this vein, I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic. These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.

Paper Structure

This paper contains 25 sections, 15 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Background
  3. Goals
  4. Current Status and Preliminary Results
  5. Results Presented at Previous Doctoral Consortiums
  6. Conditional literal semantics
  7. Aggregate semantics
  8. Modular proofs of correctness with aggregate constraints
  9. New Results
  10. Extending mini-gringo with conditional literals
  11. Axiomatizing new aggregates
  12. Recursive aggregates
  13. Program to program verification
  14. Anthem 2
  15. Ongoing Directions and Expected Achievements
  16. ...and 10 more sections

Figures (1)

  • Figure 1: Universes corresponding to the sorts used in standard interpretations fan22.