RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
  
search:
  
fwf

SToUT: Symbolic Computation Techniques for Unranked Terms


Supported by the Austrian Science Fund (FWF), Project P 24087-N18 (2012-2015)


Short Description

Languages over unranked alphabets attracted considerable attention in recent years because of their wide range of applications. They naturally model XML documents, program schemata, ambients, multithreaded recursive program configurations where the number of parallel processes is unbounded, variadic functions in various programming languages, etc. They appear also in the areas like rewriting, knowledge representation, program analysis and transformation, just to name a few.

The unranked terms we are interested in may contain context and hedge variables, the order of arguments of some function symbols may be irrelevant, regular languages may appear in sorts or in constraints for some variables. Such a framework is rich enough to model interesting applications.

Research on symbolic computation techniques (solving, proving, computing) for unranked terms does not have a long history. In this project we are concerned with the solving aspect because of its fundamental importance. In particular, we focus on two dual techniques: Unification and anti-unification. They will be studied for first-order and second-order expressions, with and without sorts, syntactically and modulo an equational theory. The general goal is to design algorithms and procedures, to analyze them, to study efficient special cases, to implement, and to apply in interesting "real-world" problems.

Team

Software

The paper that describes the library of the anti-unification algorithms listed above.

Refereed Publications

  1. A. Baumgartner, T. Kutsia. Unranked Second-Order Anti-Unification. Information and Computation. To appear. DOI: 10.1016/j.ic.2017.01.005.
  2. A. Baumgartner, T. Kutsia, J. Levy, M. Villaret. Higher-Order Pattern Anti-Unification in Linear Time. Journal of Automated Reasoning. 58(2):293–310, 2017. DOI: 10.1007/s10817-016-9383-3.
    PDF, BibTeX.
  3. B. Dundua, T. Kutsia, K. Reisenberger-Hagmayr. An overview of PρLog. In: Y. Lierler and W. Taha, editors. Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017. Volume 10137 of of Lecture Notes in Computer Science. Springer, 2017. 34–49. © Springer.
    PDF, BibTeX.
  4. B. Dundua, T. Kutsia, K. Reisenberger-Hagmayr. PρLog: Combining Logic Programming with Conditional Transformation Systems (Tool Description). In: M. Carro, A. King, N. Saeedloei, and M. De Vos, editors. Technical Communications of the 32nd International Conference on Logic Programming, ICLP 2016. Vol. 52 of OpenAccess Series in Informatics (OASIcs). Schloss Dagstuhl, 2016, 10.1–10.5.
    PDF, BibTeX.
  5. B. Konev, T. Kutsia. Anti-Unification of Concepts in Description Logic EL. In: Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, KR 2016. April 25–29, 2016, Cape Town, South Africa. The AAAI Press, 2016. 227–236.
    PDF, BibTeX.
  6. M. Marin, T. Kutsia, B. Dundua. A Rewrite-based Computational Model for Functional Logic Programming. In: J. H. Davenport and F. Ghourabi, editors. Proceedings of the 7th International Symposium on Symbolic Computation in Software Science, SCSS 2016. EPiC Series, Volume 39, EasyChair, 2016. 95–106.
    PDF, BibTeX.
  7. B. Dundua, M. Florido, T. Kutsia, M. Marin. CLP(H): Constraint Logic Programming for Hedges. Theory and Practice of Logic Programming. 16(2):141–162, 2016.
    PDF, BibTeX.
  8. B. Dundua, M. Florido, T. Kutsia. Lambda Calculus with Regular Types. In: Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2015. September 21–24, 2015, Timisoara, Romania. IEEE Computer Society, © IEEE, 2015, 129–136.
    PDF, BibTeX.
  9. I. Kotsireas, T. Kutsia, D. Simos. Constructing Orthogonal Designs in Powers of Two: Gröbner Bases Meet Equational Unification. In M. Fernández, editor, Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA 2015. June 29–July 3, 2015, Warsaw, Poland. Vol. 36 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2015, 241–256.
    PDF, PDF (with appendix), BibTeX.
  10. A. Baumgartner, T. Kutsia, J. Levy, M. Villaret. Nominal Anti-Unification. In M. Fernández, editor, Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA 2015. June 29–July 3, 2015, Warsaw, Poland. Vol. 36 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2015, 57–73.
    PDF, BibTeX.
  11. T. Kutsia, M. Marin. Regular Expression Order-Sorted Unification and Matching. J. Symbolic Computation. 67:42–67, 2015.
    PDF, BibTeX.
  12. A. Baumgartner, T. Kutsia. A Library of Anti-Unification Algorithms. In: E. Ferme and J. Leite, editors, Proceedings of the 14th European Conference on Logics in Artificial Intelligence, JELIA 2014. September 24–26, Madeira, Portugal. Volume 8761 of Lecture Notes in Computer Science. Springer, 2014, 543–557. © Springer.
    PDF, BibTeX.
  13. A. Baumgartner, T. Kutsia. Unranked Second-Order Anti-Unification. In: U. Kohlenbach, editor, Proceedings of the 21st Workshop on Logic, Language, Information and Computation, WoLLIC 2014. September 4–6, 2014, Valparaiso, Chile. Volume 8652 of Lecture Notes in Computer Science. Springer, 2014, 66–80. © Springer.
    PDF, BibTeX.
  14. B. Dundua, M. Florido, T. Kutsia, M. Marin. Constraint Logic Programming for Hedges: A Semantic Reconstruction. In: M. Codish and E. Sumii, editors, Proceedings of the 12th International Symposium on Functional and Logic Programming, FLOPS 2014. June 4–6, 2014, Kanazawa, Japan. Volume 8475 of Lecture Notes in Computer Science. Springer, 2014, 285–301. © Springer.
    PDF, BibTeX.
  15. T. Kutsia, J. Levy, M. Villaret. Anti-Unification for Unranked Terms and Hedges. J. Automated Reasoning. 52(2):155–190, 2014.
    PDF, BibTeX.
  16. A. Baumgartner, T. Kutsia, J. Levy, M. Villaret. A Variant of Higher-Order Anti-Unification. In: F. van Raamsdonk, editor, Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013. June 24–26, 2013, Eindhoven, The Netherlands. Vol. 21 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2013, 113–127.
    PDF, BibTeX.
  17. T. Kutsia, M. Marin. Solving, Reasoning, and Programming in Common Logic. In: Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012. September 26-29, 2012, Timisoara, Romania. IEEE Computer Society. © IEEE, 2013, 119–126.
    PDF, BibTeX.

PhD Thesis

  1. A. Baumgartner. Anti-Unification Algorithms: Design, Analysis, and Implementation. RISC, JKU Linz. PhD Thesis. September 2015.
    PDF.

Papers in Informal Proceedings

  1. A. Baumgartner, T. Kutsia, J. Levy, M. Villaret. Nominal Anti-unification. In: T. Kutsia and Ch. Ringeissen, editors. 28th International Workshop on Unification, UNIF 2014. July 13, 2014, Vienna, Austria. 62–69.
  2. S. Alves, B. Dundua, M. Florido, and T. Kutsia. A Confluent Pattern Calculus with Hedge Variables. In: N. Hirokawa and V. van Oostrom, editors, 2nd International Workshop on Confluence, IWC 2013. June 28, 2013, 41–45, Eindhoven, The Netherlands.
  3. T. Kutsia. Anti-Unification: Algorithms and Applications (Invited Talk). In: B. Morawska and K. Korovin, editors, 27th International Workshop on Unification, UNIF 2013. June 27, 2013, p.2, Eindhoven, The Netherlands.
  4. A. Baumgartner and T. Kutsia. Unranked Anti-Unification with Hedge and Context Variables. In: B. Morawska and K. Korovin, editors, 27th International Workshop on Unification, UNIF 2013. June 27, 2013, 13–21, Eindhoven, The Netherlands.

All Project-Related Activities

From the RISC Web page, one can get the list of all activities related to this project following this link.

Contact

Temur Kutsia (Project leader)
Research Institute for Symbolic Computation
Johannes Kepler University Linz
Altenbergerstrasse 69
A-4040 Linz, Austria
Phone: +43 (0)732 2468 9982
kutsia@risc.jku.at