Formal Methods for Optimizing Nonmonotonic Logic Programs

Nonmonotonic logic programs are an important computing approach for solving complex search problems in a declarative way. In particular, logic programs under the answer-set semantics enjoy an increasing importance in recent years, mainly due to the availability of efficient solvers. Despite the high sophistication of these tools, there are still several shortcomings of the answer-set semantics as a general programming paradigm, especially what concerns simplification and optimization issues. In this project, we want to address these issues by researching formal methods for comparing and optimizing nonmonotonic logic programs under the answer-set semantics. In particular, based on a systematic exploration of different notions of equivalences, which are important for program optimization, a general framework for specifying equivalences, encompassing all currently known forms of equivalence, should be provided, constituting the theoretical underpinning for general methods for optimization. This includes the investigation of formal properties, like semantical and computational characterizations, of the introduced concepts. The developed methods shall be applied on concrete application fields, and suitable procedures shall be implemented yielding prototype modules for automated program optimization. These tools should then provide the basis for supporting programmers for debugging and verification needs, as well as for aiding modular programming.

Nonmonotonic logic programs are an important computing approach for solving complex search problems in a declarative way. In particular, logic programs under the answer-set semantics enjoy an increasing importance in recent years, mainly due to the availability of efficient solvers. Despite the high sophistication of these tools, there are still several shortcomings of the answer-set semantics as a general programming paradigm, especially what concerns simplification and optimization issues. In this project, we want to address these issues by researching formal methods for comparing and optimizing nonmonotonic logic programs under the answer-set semantics. In particular, based on a systematic exploration of different notions of equivalences, which are important for program optimization, a general framework for specifying equivalences, encompassing all currently known forms of equivalence, should be provided, constituting the theoretical underpinning for general methods for optimization. This includes the investigation of formal properties, like semantical and computational characterizations, of the introduced concepts. The developed methods shall be applied on concrete application fields, and suitable procedures shall be implemented yielding prototype modules for automated program optimization. These tools should then provide the basis for supporting programmers for debugging and verification needs, as well as for aiding modular programming.