Equivalence Checking Between Logic Programs with Aggregates in ASP

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Equivalence Checking Between Logic Programs with Aggregates in ASP

Vortrag von Rowan Rosenberg
Answer Set Programming (ASP) is a form of declarative programming. It is used in a range of practical applications in problem solving tasks, which has continued to expand in recent years. Equivalence checking is useful to determine whether modifications to a program preserve the intended meaning, or when evaluating a program’s semantic correctness according to the standard of another. Determining whether complex ASP programs represent the same knowledge can be difficult and there are different senses of equivalence which can be applied. The current state-of-the-art in equivalence checking of ASP programs is ANTHEM 2.0. ANTHEM provides automated equivalence checking over a subset of ASP programs, but does not support several common program features such as, aggregates, strong negation, and positive recursion. This project aims to extend ANTHEM toward complete coverage of the languages of ASP solvers clingo and DLV, which are the predominant tools for evaluating ASP programs. This has the potential to benefit future ASP research, such as that involving automated ASP generation, as well as ASP programming in practice.