Skip to Content

TU Wien Fakultät für Informatik Knowledge-Based Systems Group
Top-level Navigation: Current-level Navigation:

Path: KBS > research > projects > eq >

Tools: Drucken

Project: Formal Methods for Comparing and Optimizing Nonmonotonic Logic Programs

(supported by the Austrian Science Foundation under grant P18019-N04.)

The project was finished by December 2008.

Contents

Project team

Project Leader:

Project Staff:

Project Participants:

Students:

Former Staff Members:

Project synopsis

Nonmonotonic logic programs represent an import method for declarative problem solving, gaining an increasing importance in the last years, which is mainly due to the availability of efficient solvers. In this project, we studied formal methods for comparing and optimizing nonmonotonic logic programs under the answer-set semantics. In particular, we defined a general framework for specifying equivalence notions, which provides the formal underpinning for program optimization and other programming engineering tasks. Furthermore, novel semantical structures for characterizing different relevant equivalence notions have been introduced, along with the development of various program simplification techniques and a comprehensive analysis of their computational complexity. The development of concrete systems for computing different tasks studied in the context of the project, as well as a case study for program verification, round off the project results.

Goal of the project

The goal of this project is to research 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, a general framework for specifying equivalences, encompassing all currently known forms of program 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.

Software

Publications

2009

[1] Merging Logic Programs under Answer Set Semantics.
James P. Delgrande, Torsten Schaub, Hans Tompits, and Stefan Woltran.
In Patricia M. Hill and David S. Warren, editors, Proceedings of the Twenty-Fifth International Conference on Logic Programming, (ICLP'09), Pasadena, CA, USA, July 14-17, 2009, volume 5649 of Lecture Notes in Computer Science, pages 160–174. Springer, 2009. [ bib | .pdf | .ps ]
[2] Modularity Aspects of Disjunctive Stable Models.
Tomi Janhunen, Emilia Oikarinen, Hans Tompits, and Stefan Woltran.
To appear in Journal of Artificial Intelligence Research, 2009. [ bib | .pdf | .ps ]
[3] ccT on Stage: Generalised Uniform Equivalence Testing for Verifying Student Assignment Solutions.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
To appear in Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'09), Potsdam, Germany, 2009. [ bib | .ps | .pdf ]
[4] Characterising Equilibrium Logic and Nested Logic Programs: Reductions and Complexity.
David Pearce, Hans Tompits, and Stefan Woltran.
To appear in Theory and Practice of Logic Programming, 2009. [ bib | .pdf | .ps ]
[5] Casting Away Disjunction and Negation under a Generalisation of Strong Equivalence with Projection.
Jörg Pührer and Hans Tompits.
To appear in Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'09), Potsdam, Germany, 2009. [ bib | .ps | .pdf ]

2008

[1] Elimination of Disjunction and Negation in Answer-Set Programs under Hyperequivalence.
Jörg Pührer, Hans Tompits, and Stefan Woltran.
In Maria G. de la Banda and Enrico Pontelli, editors, Proceedings of the Twenty-Fourth International Conference on Logic Programming, (ICLP'08), Udine, Italy, December 9-13, 2008, volume 5366 of Lecture Notes in Computer Science, pages 561–575. Springer, 2008. [ bib | .pdf | .ps ]
[2] Program Correspondence under the Answer-Set Semantics: The Non-Ground Case.
Johannes Oetsch and Hans Tompits.
In Maria G. de la Banda and Enrico Pontelli, editors, Proceedings of the Twenty-Fourth International Conference on Logic Programming, (ICLP'08), Udine, Italy, December 9-13, 2008, volume 5366 of Lecture Notes in Computer Science, pages 591–605. Springer, 2008. [ bib | .pdf | .ps ]
[3] Relativized Hyperequivalence of Logic Programs for Modular Programming.
Mirosław Truszczyński and Stefan Woltran.
In Maria G. de la Banda and Enrico Pontelli, editors, Proceedings of the Twenty-Fourth International Conference on Logic Programming, (ICLP'08), Udine, Italy, December 9-13, 2008, volume 5366 of Lecture Notes in Computer Science, pages 576–590. Springer, 2008. [ bib | .pdf | .ps ]
[4] Belief Revision of Logic Programs under Answer Set Semantics.
James P. Delgrande, Torsten Schaub, Hans Tompits, and Stefan Woltran.
In Gerhard Brewka and Jérôme Lang, editors, Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR'08), Sydney, Australia, September 16-19, 2008, pages 411–421. AAAI Press, 2008.
[ bib | .ps | .pdf ]
[5] Notions of Strong Equivalence for Logic Programs with Ordered Disjunction.
Wolfgang Faber, Hans Tompits, and Stefan Woltran.
In Gerhard Brewka and Jérôme Lang, editors, Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR'08), Sydney, Australia, September 16-19, 2008, pages 433–443. AAAI Press, 2008.
[ bib | .ps | .pdf ]
[6] A Meta-Programming Technique for Debugging Answer-Set Programs.
Martin Gebser, Jörg Pührer, Torsten Schaub, and Hans Tompits.
In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (AAAI'08), Chicago, Illinois, USA, July 13-17, 2008, pages 448–453. AAAI Press, 2008. [ bib | .ps | .pdf ]
[7] Hyperequivalence of Logic Programs with Respect to Supported Models.
Mirosław Truszczyński and Stefan Woltran.
In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (AAAI'08), Chicago, Illinois, USA, July 13-17, 2008, pages 560–565. AAAI Press, 2008. [ bib | .ps | .pdf ]
[8] Alternative Characterizations for Program Equivalence under Answer-Set Semantics Based on Unfounded Sets.
Martin Gebser, Torsten Schaub, Hans Tompits, and Stefan Woltran.
In Sven Hartmann and Gabriele Kern-Isberner, editors, Proceedings of the 5th International Symposium on Foundations of Information and Knowledge Systems (FoIKS'08), Pisa, Italy, February 11-15, volume 4932 of Lecture Notes in Computer Science, pages 24–41. Springer, 2008. [ bib | .ps | .pdf ]
[9] A Common View on Strong, Uniform, and Other Notions of Equivalence in Answer-Set Programming.
Stefan Woltran.
Theory and Practice of Logic Programming, 8(2):217–234, 2008. [ bib | .ps | .pdf ]

2007

[1] Debugging ASP Programs by Means of ASP.
Martin Brain, Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, and Stefan Woltran.
In Chitta Baral, Gerhard Brewka, and John Schlipf, editors, Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07), Tempe, AZ, USA, volume 4483 of Lecture Notes in Artificial Intelligence, pages 31–43. Springer, 2007. [ bib | .ps | .pdf ]
[2] “That is Illogical Captain!” – The Debugging Support Tool spock for Answer-Set Programs: System Description.
Martin Brain, Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, and Stefan Woltran.
In Marina De Vos and Torsten Schaub, editors, Proceedings of the 1st International Workshop on Software Engineering for Answer-Set Programming (SEA'07), Tempe, AZ, USA, pages 71–85, 2007. [ bib | .ps | .pdf ]
[3] Complexity results for answer set programming with bounded predicate arities and implications.
Thomas Eiter, Wolfgang Faber, Michael Fink, and Stefan Woltran.
Annals of Mathematics and Artificial Intelligence, 51:123–165, 2007. [ bib | .ps | .pdf ]
[4] Complexity Results for Checking Equivalence of Stratified Logic Programs.
Thomas Eiter, Michael Fink, Hans Tompits, and Stefan Woltran.
In Manuela M. Veloso, editor, IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI'07), Hyderabad, India, January 6-12, 2007, pages 330–335, 2007. [ bib | .ps | .pdf ]
[5] Semantical Characterizations and Complexity of Equivalences in Answer Set Programming.
Thomas Eiter, Michael Fink, and Stefan Woltran.
ACM Transactions on Computational Logic, 8(3):17, 2007. [ bib | .ps | .pdf ]
[6] Characterizing Notions of Strong Equivalence for Logic Programs with Ordered Disjunctions.
Wolfgang Faber, Hans Tompits, and Stefan Woltran.
In Proceedings of the 3rd Multidisciplinary Workshop on Advances in Preference Handling (M-PREF'07), 2007. [ bib | .ps | .pdf ]
[7] Complexity of Rule Redundancy in Non-ground Answer-Set Programming over Finite Domains.
Michael Fink, Reinhard Pichler, Hans Tompits, and Stefan Woltran.
In Chitta Baral, Gerhard Brewka, and John Schlipf, editors, Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07), Tempe, AZ, USA, volume 4483 of Lecture Notes in Artificial Intelligence, pages 31–43. Springer, 2007. [ bib | .ps | .pdf ]
[8] spock: A Debugging Support Tool for Logic Programs under the Answer-Set Semantics.
Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, and Stefan Woltran.
In Dietmar Seipel, Michael Hanus, Armin Wolf, and Joachim Baumeister, editors, Proceedings of the 21st Workshop on (Constraint) Logic Programming, (WLP'07), Würzburg, Germany, pages 258–261. Technical Report 434, Bayerische Julius-Maximilians-Universität Würzburg, Institut für Informatik, 2007. [ bib | .ps | .pdf ]
[9] Alternative Characterizations for Program Equivalence under Answer-Set Semantics: Preliminary Report.
Martin Gebser, Torsten Schaub, Hans Tompits, and Stefan Woltran.
In David Pearce, Axel Polleres, Agustín Valverde, and Stefan Woltran, editors, Proceedings of the LPNMR'07 Workshop on Correspondence and Equivalence for Nonmonotonic Theories (CENT'07), Tempe, AZ, May 14, 2007, volume 265 of CEUR Workshop Proceedings. CEUR-WS.org, 2007. [ bib | .ps | .pdf ]
[10] Modularity Aspects of Disjunctive Stable Models.
Tomi Janhunen, Emilia Oikarinen, Hans Tompits, and Stefan Woltran.
In Chitta Baral, Gerhard Brewka, and John Schlipf, editors, Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07), Tempe, AZ, USA, volume 4483 of Lecture Notes in Artificial Intelligence, pages 31–43. Springer, 2007. [ bib | .ps | .pdf ]
[11] An Extension of the System ccT for Testing Relativised Uniform Equivalence under Answer-Set Projection.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
In Proceedings of the 16th International Conference on Computing (CIC'07). IEEE Computer Society Press, 2007. [ bib | .ps | .pdf ]
[12] Testing Relativised Uniform Equivalence under Answer-Set Projection in the System ccT.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
In Dietmar Seipel, Michael Hanus, Armin Wolf, and Joachim Baumeister, editors, Proceedings of the 21st Workshop on (Constraint) Logic Programming, (WLP'07), Würzburg, Germany, pages 254–257. Technical Report 434, Bayerische Julius-Maximilians-Universität Würzburg, Institut für Informatik, 2007. [ bib | .ps | .pdf ]
[13] Facts do not Cease to Exist Because They are Ignored: Relativised Uniform Equivalence with Answer-Set Projection.
Johannes Oetsch, Hans Tompits, and Stefan Woltran.
In David Pearce, Axel Polleres, Agustín Valverde, and Stefan Woltran, editors, Proceedings of the LPNMR'07 Workshop on Correspondence and Equivalence for Nonmonotonic Theories (CENT'07), Tempe, AZ, May 14, 2007, volume 265 of CEUR Workshop Proceedings. CEUR-WS.org, 2007. [ bib | .ps | .pdf ]
[14] Facts do not Cease to Exist Because They are Ignored: Relativised Uniform Equivalence with Answer-Set Projection.
Johannes Oetsch, Hans Tompits, and Stefan Woltran.
In Proceedings of the 22nd National Conference on Artificial Intelligence (AAAI'07), pages 458–464. AAAI Press, 2007. [ bib | .ps | .pdf ]
[15] Characterising Equilibrium Logic and Nested Logic Programs: Reductions and Complexity.
David Pearce, Hans Tompits, and Stefan Woltran.
Technical report, Universidad Rey Juan Carlos, Grupo de Inteligencia Artificial, 2007. Accepted for publication in Theory and Practice of Logic Programming (TPLP). [ bib | .ps | .pdf ]
[16] Relativised Equivalence in Equilibrium Logic and its Applications to Prediction and Explanation: Preliminary Report.
David Pearce, Hans Tompits, and Stefan Woltran.
In David Pearce, Axel Polleres, Agustín Valverde, and Stefan Woltran, editors, Proceedings of the LPNMR'07 Workshop on Correspondence and Equivalence for Nonmonotonic Theories (CENT'07), Tempe, AZ, May 14, 2007, volume 265 of CEUR Workshop Proceedings. CEUR-WS.org, 2007. [ bib | .ps | .pdf ]
[17] A Common View on Strong, Uniform, and Other Notions of Equivalence in Answer-Set Programming.
Stefan Woltran.
In David Pearce, Axel Polleres, Agustín Valverde, and Stefan Woltran, editors, Proceedings of the LPNMR'07 Workshop on Correspondence and Equivalence for Nonmonotonic Theories (CENT'07), Tempe, AZ, May 14, 2007, volume 265 of CEUR Workshop Proceedings. CEUR-WS.org, 2007. [ bib | .ps | .pdf ]

2006

[1] Replacements in Non-Ground Answer-Set Programming.
Thomas Eiter, Michael Fink, Hans Tompits, Patrick Traxler, and Stefan Woltran.
In Patrick Doherty, John Mylopoulos, and Christopher A. Welty, editors, Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR'06), Lake District of the United Kingdom, June 2-5, pages 340–351. AAAI Press, 2006. [ bib | .ps | .pdf ]
[2] Replacements in Non-Ground Answer-Set Programming.
Thomas Eiter, Michael Fink, Hans Tompits, Patrick Traxler, and Stefan Woltran.
In Michael Fink, Hans Tompits, and Stefan Woltran, editors, Proceedings of the 20th Workshop on Logic Programming (WLP'06), Vienna, Austria, February 22–24, volume 1843-06-02 of INFSYS Research Report. Technische Universität Wien, 2006. [ bib | .ps | .pdf ]
[3] An Implementation for Recognizing Rule Replacements in Non-ground Answer-Set Programs.
Thomas Eiter, Patrick Traxler, and Stefan Woltran.
In Michael Fisher, Wiebe van der Hoek, Boris Konev, and Alexei Lisitsa, editors, Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA'06), Liverpool, UK, September 13-15, volume 4160 of Lecture Notes in Computer Science, pages 477–480. Springer, 2006. [ bib | .ps | .pdf ]
[4] A Tool for Advanced Correspondence Checking in Answer-Set Programming.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
In Jürgen Dix and Anthony Hunter, editors, Proceedings of the 11th International Workshop on Nonmonotonic Reasoning (NMR'06), Technical Report Series. Clausthal University of Technology, Institute for Informatics, 2006. [ bib | .ps | .pdf ]
[5] A Tool for Advanced Correspondence Checking in Answer-Set Programming: Preliminary Experimental Results.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
In Michael Fink, Hans Tompits, and Stefan Woltran, editors, Proceedings of the 20th Workshop on Logic Programming (WLP'06), Vienna, Austria, February 22–24, volume 1843-06-02 of INFSYS Research Report. Technische Universität Wien, 2006. [ bib | .ps | .pdf ]
[6] ccT: A correspondence-checking tool for logic programs under the answer-set semantics.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
In Michael Fisher, Wiebe van der Hoek, Boris Konev, and Alexei Lisitsa, editors, Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA'06), Liverpool, UK, September 13-15, volume 4160 of Lecture Notes in Computer Science, pages 477–480. Springer, 2006. [ bib | .ps | .pdf ]
[7] ccT: A Tool for Checking Advanced Correspondence Problems in Answer-Set Programming.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
In Alexander Gelbukh and Sergio Suárez Guerra, editors, Proceedings of the 15th International Conference on Computing (CIC'06), pages 3–10. IEEE Computer Society Press, 2006. [ bib | .ps | .pdf ]
[7] ccT: A Tool for Checking Advanced Correspondence Problems in Answer-Set Programming.
Johannes Oetsch, Martina Seidl, Hans Tompits, and Stefan Woltran.
In Proceedings of the FLOC-Workshop on Search and Logic (LaSh'06), 2006. [ bib | .ps | .pdf ]

2005

[1] Testing Strong Equivalence of Datalog Programs - Implementation and Examples.
Thomas Eiter, Wolfgang Faber, and Patrick Traxler.
In Chitta Baral, Gianluigi Greco, Nicola Leone, and Giorgio Terracina, editors, Proceedings of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), Diamante, Italy, September 5-8, volume 3662 of Lecture Notes in Computer Science, pages 437–441. Springer, 2005. [ bib | .ps | .pdf ]
[2] Strong and Uniform Equivalence in Answer-Set Programming: Characterizations and Complexity Results for the Non-Ground Case.
Thomas Eiter, Michael Fink, Hans Tompits, and Stefan Woltran.
In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings of the 20th National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference (AAAI'05), July 9-13, 2005, Pittsburgh, Pennsylvania, USA, pages 695–700. AAAI Press / The MIT Press, 2005. [ bib | .ps | .pdf ]
[3] On Solution Correspondences in Answer-Set Programming.
Thomas Eiter, Hans Tompits, and Stefan Woltran.
In Leslie P. Kaelbling and Alessandro Saffiotti, editors, Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI'05), Edinburgh, Scotland, UK, July 30-August 5, pages 97–102. Professional Book Center, 2005. [ bib | .ps | .pdf ]
[4] Towards Implementations for Advanced Equivalence Checking in Answer-Set Programming.
Hans Tompits and Stefan Woltran.
In Maurizio Gabbrielli and Gopal Gupta, editors, Proceedings of the 21st International Conference on Logic Programming (ICLP'05), Sitges, Spain, October 2-5, volume 3668 of Lecture Notes in Computer Science, pages 189–203. Springer, 2005. A preliminary version of this paper appeared in the proceedings of the ASP'05 Workshop. [ bib | .ps | .pdf ]

Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist die Fakultät für Informatik an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. / Disclaimer. Datenschutzerklärung.