Beyond Uniform Equivalence between Answer-set Programs
2021 (English)In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 22, no 1, article id 2Article in journal (Refereed) Published
Abstract [en]
This article deals with advanced notions of equivalence between nonmonotonic logic programs under the answer-set semantics, a topic of considerable interest, because such notions form the basis for program verification and are useful for program optimisation, debugging, and modular programming. In fact, there is extensive research in answer-set programming (ASP) dealing with different notions of equivalence between programs. Prominent among these notions is uniform equivalence, which checks whether two programs have the same semantics when joined with an arbitrary set of facts. In this article, we study a family of more fine-grained versions of uniform equivalence, viz. relativised uniform equivalence with projection, which extends standard uniform equivalence in terms of two additional parameters: One for specifying the input alphabet and one for specifying the output alphabet for programs. In particular, the second parameter is used for projecting answer sets to a set of designated output atoms. Answer-set projection, in particular, allows to compare programs that make use of different auxiliary atoms, which is important for practical programming aspects. We introduce novel semantic characterisations for the program correspondence problems under consideration and analyse their computational complexity. In the general case, deciding these problems lies on the third level of the polynomial hierarchy. Therefore, this task cannot be efficiently reduced to propositional answer-set programs itself (under the usual complexity-theoretic assumptions). However, reductions to quantified Boolean formulas (QBFs) are feasible. Indeed, we provide efficient (in fact, linear-time constructible) reductions to QBFs and discuss simplifications for certain special cases. These QBF reductions yield the basis for a prototype implementation, the system cc ĝŠCurrency sign, for deciding correspondence problems by using off-the-shelf QBF solvers. We discuss an application of cc ĝŠCurrency sign for verifying the correctness of solutions by students drawn from a laboratory course on logic programming and knowledge representation at the Technische Universität Wien, employing relativised uniform equivalence with projection as the underlying program correspondence notion.
Place, publisher, year, edition, pages
ACM Digital Library, 2021. Vol. 22, no 1, article id 2
Keywords [en]
Answer-set programming, disjunctive logic programs, nonmonotonic reasoning, program equivalence, quantified Boolean logic, Application programs, Boolean functions, Computer circuits, Equivalence classes, Input output programs, Knowledge representation, Logic programming, Semantics, Temporal logic, Answer set programming, Answer set semantics, Correspondence problems, Nonmonotonic logic programs, Polynomial hierarchies, Program Verification, Prototype implementations, Quantified Boolean formulas, Program debugging
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:hj:diva-63561DOI: 10.1145/3422361ISI: 000613160500002Scopus ID: 2-s2.0-85100118988OAI: oai:DiVA.org:hj-63561DiVA, id: diva2:1838528
2024-02-162024-02-162024-02-16Bibliographically approved