Symbolic Computation Techniques for Unranked Terms [SToUT]

Project Lead

Project Duration

01/06/2012 - 30/09/2016

Project URL

Go to Website

Software

This library contains unification, matching, and anti-unification algorithms in various theories developed at RISC. Unification with sequence variables. Context sequence matching. Rigid anti-unification for unranked terms and hedges and its experimental extension with commutative symbols. Unranked second-order anti-unification and its ...

MoreSoftware Website

Publications

2020

[Kutsia]

Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques

Ilias Kotsireas, Temur Kutsia, Dimitris Simos

Annals of Mathematics and Artificial Intelligence 88(1), pp. 213-236. 2020. ISSN 1573-7470. [doi] [pdf]
[bib]
@article{RISC6116,
author = {Ilias Kotsireas and Temur Kutsia and Dimitris Simos},
title = {{ Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques}},
language = {english},
journal = {Annals of Mathematics and Artificial Intelligence},
volume = {88},
number = {1},
pages = {213--236},
isbn_issn = {ISSN 1573-7470},
year = {2020},
refereed = {yes},
length = {24},
url = {https://doi.org/10.1007/s10472-018-9607-9}
}

2017

[Baumgartner]

Unranked Second-Order Anti-Unification

Alexander Baumgartner, Temur Kutsia

Information and Computation 255(2), pp. 262-286. 2017. ISSN: 0890-5401. [doi]
[bib]
@article{RISC5192,
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Unranked Second-Order Anti-Unification}},
language = {english},
journal = {Information and Computation},
volume = {255},
number = {2},
pages = {262--286},
isbn_issn = {ISSN: 0890-5401},
year = {2017},
refereed = {yes},
length = {25},
url = {http://doi.org/10.1016/j.ic.2017.01.005}
}
[Baumgartner]

Higher-Order Pattern Anti-Unification in Linear Time

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

Journal of Automated Reasoning 58(2), pp. 293-310. 2017. ISSN 0168-7433. [doi]
[bib]
@article{RISC5337,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Higher-Order Pattern Anti-Unification in Linear Time}},
language = {english},
journal = { Journal of Automated Reasoning},
volume = {58},
number = {2},
pages = {293--310},
isbn_issn = {ISSN 0168-7433},
year = {2017},
refereed = {yes},
length = {18},
url = {http://dx.doi.org/10.1007/s10817-016-9383-3}
}
[Dundua]

An overview of PρLog

Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayr

In: Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017, Y. Lierler and W. Taha (ed.), Lecture Notes in Computer Science 10137, pp. 34-49. 2017. Springer, ISBN 978-3-319-51675-2. [pdf]
[bib]
@inproceedings{RISC5416,
author = {Besik Dundua and Temur Kutsia and Klaus Reisenberger-Hagmayr},
title = {{An overview of PρLog}},
booktitle = {{ Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10137},
pages = {34--49},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-51675-2},
year = {2017},
editor = {Y. Lierler and W. Taha},
refereed = {yes},
length = {16}
}
[Dundua]

Pattern-Based Calculi with Finitary Matching

Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia

Logic Journal of the IGPL, pp. -. 2017. Oxford University Press, ISSN 1367-0751. To appear. [doi]
[bib]
@article{RISC5517,
author = {Sandra Alves and Besik Dundua and Mario Florido and Temur Kutsia},
title = {{Pattern-Based Calculi with Finitary Matching}},
language = {english},
journal = {Logic Journal of the IGPL},
pages = {--},
publisher = {Oxford University Press},
isbn_issn = {ISSN 1367-0751},
year = {2017},
note = {To appear},
refereed = {yes},
length = {41},
url = {https://doi.org/10.1093/JIGPAL/jzx059}
}
[Kutsia]

Nominal Unification of Higher Order Expressions with Recursive Let

Manfred Schmidt-Schauss, Temur Kutsia, Jordy Levy, Mateu Villaret

In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016, M. Hermenegildo and P. Lopez-Garcia (ed.), LNCS 10184, pp. 328-344. 2017. Springer, ISBN 978-3-319-63138-7. [pdf]
[bib]
@inproceedings{RISC5438,
author = {Manfred Schmidt-Schauss and Temur Kutsia and Jordy Levy and Mateu Villaret},
title = {{Nominal Unification of Higher Order Expressions with Recursive Let}},
booktitle = {{ Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016}},
language = {english},
series = {LNCS},
volume = {10184},
pages = {328--344},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-63138-7},
year = {2017},
editor = {M. Hermenegildo and P. Lopez-Garcia},
refereed = {yes},
length = {17}
}

2016

[Dundua]

CLP(H): Constraint Logic Programming for Hedges

Besik Dundua, Mario Florido, Temur Kutsia, Mircea Marin

Theory and Practice of Logic Programming 16(2), pp. 141-162. 2016. ISSN 1471-0684. [url]
[bib]
@article{RISC5133,
author = {Besik Dundua and Mario Florido and Temur Kutsia and Mircea Marin},
title = {{CLP(H): Constraint Logic Programming for Hedges}},
language = {english},
journal = {Theory and Practice of Logic Programming},
volume = {16},
number = {2},
pages = {141--162},
isbn_issn = {ISSN 1471-0684},
year = {2016},
refereed = {yes},
sponsor = {FWF under the project P 24087-N18},
length = {22},
url = {http://arxiv.org/abs/1503.00336}
}
[Dundua]

A rewrite-based computational model for functional logic programming

Mircea Marin, Temur Kutsia, Besik Dundua

In: Proceedings of the 7th International Symposium on Symbolic Computation in Software Science, SCSS 2016, James H. Davenport (ed.), EPiC Series in Computing 39, pp. 95-106. 2016. EasyChair, ISSN 2398-7340. [url]
[bib]
@inproceedings{RISC5336,
author = {Mircea Marin and Temur Kutsia and Besik Dundua},
title = {{A rewrite-based computational model for functional logic programming}},
booktitle = {{Proceedings of the 7th International Symposium on Symbolic Computation in Software Science, SCSS 2016}},
language = {english},
series = {EPiC Series in Computing},
volume = {39},
pages = {95--106},
publisher = {EasyChair},
isbn_issn = {ISSN 2398-7340},
year = {2016},
editor = {James H. Davenport},
refereed = {yes},
length = {12},
url = {http://www.easychair.org/publications/download/A_rewrite-based_computational_model_for_functional_logic_programming}
}
[Dundua]

An Overview of PρLog

Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayer

Technical report no. 16-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2016. [pdf]
[bib]
@techreport{RISC5349,
author = {Besik Dundua and Temur Kutsia and Klaus Reisenberger-Hagmayer},
title = {{An Overview of PρLog}},
language = {english},
number = {16-05},
year = {2016},
length = {18},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Dundua]

PρLog: Combining Logic Programming with Conditional Transformation Systems (Tool Description)

B. Dundua, T. Kutsia, K. Reisenberger-Hagmayr

In: Technical Communications of the 32nd International Conference on Logic Programming, ICLP 2016, M. Carro, A. King, N. Saeedloei, and M. De Vos (ed.), OpenAccess Series in Informatics (OASIcs) 52, pp. 10.1-10.5. 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, ISBN 978-3-95977-007-1, ISSN 2190-6807. [url]
[bib]
@inproceedings{RISC5415,
author = {B. Dundua and T. Kutsia and K. Reisenberger-Hagmayr},
title = {{PρLog: Combining Logic Programming with Conditional Transformation Systems (Tool Description)}},
booktitle = {{Technical Communications of the 32nd International Conference on Logic Programming, ICLP 2016}},
language = {english},
series = {OpenAccess Series in Informatics (OASIcs)},
volume = {52},
pages = {10.1--10.5},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
isbn_issn = {ISBN 978-3-95977-007-1, ISSN 2190-6807},
year = {2016},
editor = {M. Carro and A. King and N. Saeedloei and and M. De Vos},
refereed = {yes},
length = {5},
url = {http://drops.dagstuhl.de/opus/volltexte/2016/6740/pdf/OASIcs-ICLP-2016-10.pdf}
}
[Konev]

Anti-Unification of Concepts in Description Logic EL

Boris Konev, Temur Kutsia

In: Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, KR 2016, Chitta Baral, James P. Delgrande, Frank Wolter (ed.), pp. 227-236. April 25-29 2016. AAAI Press, Cape Town, South Africa, 978-1-57735-755-1. [url]
[bib]
@inproceedings{RISC5281,
author = {Boris Konev and Temur Kutsia},
title = {{Anti-Unification of Concepts in Description Logic EL}},
booktitle = {{Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, KR 2016}},
language = {english},
pages = {227--236},
publisher = {AAAI Press},
address = {Cape Town, South Africa},
isbn_issn = {978-1-57735-755-1},
year = {2016},
month = {April 25--29},
editor = {Chitta Baral and James P. Delgrande and Frank Wolter},
refereed = {yes},
length = {10},
url = {http://www.aaai.org/ocs/index.php/KR/KR16/paper/download/12880/12479}
}
[Kutsia]

Nominal Unification of Higher Order Expressions with Recursive Let

Manfred Schmidt-Schauss, Temur Kutsia, Jordi Levy, Mateu Villaret

Technical report no. 16-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2016. [pdf]
[bib]
@techreport{RISC5292,
author = {Manfred Schmidt-Schauss and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Nominal Unification of Higher Order Expressions with Recursive Let}},
language = {english},
number = {16-03},
year = {2016},
length = {15},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Maletzky]

Theorema 2.0: Computer-Assisted Natural-Style Mathematics

Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger

JFR 9(1), pp. 149-185. 2016. ISSN 1972-5787. [doi]
[bib]
@article{RISC5243,
author = {Bruno Buchberger and Tudor Jebelean and Temur Kutsia and Alexander Maletzky and Wolfgang Windsteiger},
title = {{Theorema 2.0: Computer-Assisted Natural-Style Mathematics}},
language = {english},
abstract = {The Theorema project aims at the development of a computer assistant for the working mathematician. Support should be given throughout all phases of mathematical activity, from introducing new mathematical concepts by definitions or axioms, through first (computational) experiments, the formulation of theorems, their justification by an exact proof, the application of a theorem as an algorithm, until to the dissemination of the results in form of a mathematical publication, the build up of bigger libraries of certified mathematical content and the like. This ambitious project is exactly along the lines of the QED manifesto issued in 1994 (see e.g. http://www.cs.ru.nl/~freek/qed/qed.html) and it was initiated in the mid-1990s by Bruno Buchberger. The Theorema system is a computer implementation of the ideas behind the Theorema project. One focus lies on the natural style of system input (in form of definitions, theorems, algorithms, etc.), system output (mainly in form of mathematical proofs) and user interaction. Another focus is theory exploration, i.e. the development of large consistent mathematical theories in a formal frame, in contrast to just proving single isolated theorems. When using the Theorema system, a user should not have to follow a certain style of mathematics enforced by the system (e.g. basing all of mathematics on set theory or certain variants of type theory), rather should the system support the user in her preferred flavour of doing math. The new implementation of the system, which we refer to as Theorema 2.0, is open-source and available through GitHub.},
journal = {JFR},
volume = {9},
number = {1},
pages = {149--185},
isbn_issn = {ISSN 1972-5787},
year = {2016},
refereed = {yes},
keywords = {Mathematical assistant systems, Theorema, automated reasoning, theory exploration, unification},
length = {37},
url = {http://dx.doi.org/10.6092/issn.1972-5787/4568}
}
[Schreiner]

Predicting Space Requirements for a Stream Monitor Specification Language

David M. Cerna and Wolfgang Schreiner, Temur Kutsia

In: Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings, Yli{\`{e}}s Falcone and C{\'{e}}sar S{\'{a}}nchez (ed.), pp. 135-151. 2016. 978-3-319-46981-2. [doi]
[bib]
@inproceedings{RISC5739,
author = {David M. Cerna and Wolfgang Schreiner and Temur Kutsia},
title = {{Predicting Space Requirements for a Stream Monitor Specification Language}},
booktitle = {{Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings}},
language = {english},
pages = {135--151},
isbn_issn = {978-3-319-46981-2},
year = {2016},
editor = {Yli{\`{e}}s Falcone and C{\'{e}}sar S{\'{a}}nchez},
refereed = {yes},
length = {17},
url = {https://doi.org/10.1007/978-3-319-46982-9_9}
}

2015

[Baumgartner]

Nominal Anti-Unification

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

RISC. Technical report no. 15-03, April 2015. [pdf]
[bib]
@techreport{RISC5145,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Nominal Anti-Unification}},
language = {english},
number = {15-03},
year = {2015},
month = {April},
institution = {RISC},
length = {28}
}
[Baumgartner]

Nominal Anti-Unification

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA'15, Maribel Fernandez (ed.), Leibniz International Proceedings in Informatics (LIPIcs) , pp. 57-73. 2015. ISSN 1868-8969. [pdf]
[bib]
@inproceedings{RISC5149,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Nominal Anti-Unification}},
booktitle = {{Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA'15}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
pages = {57--73},
isbn_issn = {ISSN 1868-8969},
year = {2015},
editor = {Maribel Fernandez},
refereed = {yes},
sponsor = {FWF under the project P 24087-N18},
length = {17}
}
[Baumgartner]

Anti-Unification Algorithms: Design, Analysis, and Implementation

Alexander Baumgartner

RISC, JKU Linz. PhD Thesis. September 2015. [pdf]
[bib]
@phdthesis{RISC5180,
author = {Alexander Baumgartner},
title = {{Anti-Unification Algorithms: Design, Analysis, and Implementation}},
language = {english},
year = {2015},
month = {September},
translation = {0},
school = {RISC, JKU Linz},
length = {169}
}
[Dundua]

Lambda Calculus with Regular Types

Besik Dundua, Mario Florido, Temur Kutsia

In: Proceeding of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2015, , pp. -. 2015. To appear. [pdf]
[bib]
@inproceedings{RISC5168,
author = {Besik Dundua and Mario Florido and Temur Kutsia},
title = {{Lambda Calculus with Regular Types}},
booktitle = {{Proceeding of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2015}},
language = {english},
pages = {--},
isbn_issn = { },
year = {2015},
note = {To appear},
editor = { },
refereed = {yes},
length = {0}
}
[Konev]

Anti-Unification of Concepts in Description Logic EL

Boris Konev, Temur Kutsia

Technical report no. 15-20 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2015. [pdf]
[bib]
@techreport{RISC5266,
author = {Boris Konev and Temur Kutsia},
title = {{Anti-Unification of Concepts in Description Logic EL}},
language = {english},
number = {15-20},
year = {2015},
length = {15},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Kutsia]

Constructing Orthogonal Designs in Powers of Two: Groebner Bases Meet Equational Unification

Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos

In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA'15, Maribel Fernandez (ed.), Leibniz International Proceedings in Informatics (LIPIcs) , pp. 241-256. 2015. Schloss Dagstuhl, ISSN 1868-8969. [pdf]
[bib]
@inproceedings{RISC5143,
author = {Ilias Kotsireas and Temur Kutsia and Dimitris E. Simos},
title = {{Constructing Orthogonal Designs in Powers of Two: Groebner Bases Meet Equational Unification}},
booktitle = {{Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA'15}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
pages = {241--256},
publisher = {Schloss Dagstuhl},
isbn_issn = {ISSN 1868-8969},
year = {2015},
editor = {Maribel Fernandez},
refereed = {yes},
sponsor = {FWF under the project P 24087-N18},
length = {16}
}

Loading…