Rewriting-related Techniques and Applications

@inproceedings{RISC5707,
author = {N. Amiridze and T. Kutsia},
title = {{Anti-Unification and Natural Language Processing}},
booktitle = {{Fifth Workshop on Natural Language and Computer Science, NLCS’18}},
language = {english},
series = {EasyChair preprints},
number = {203},
pages = {1--12},
isbn_issn = { },
year = {2018},
editor = {A. Asudeh and V. de Paiva and L. Moss},
refereed = {yes},
length = {12},
url = {https://doi.org/10.29007/fkrh}
}

@inproceedings{RISC5733,
author = {A. Maletzky and F. Immler},
title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL}},
booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17)}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {11006},
pages = {178--193},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-96811-7},
year = {2018},
note = {The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16},
editor = {Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef},
refereed = {yes},
length = {16},
conferencename = {CICM 2018},
url = {https://doi.org/10.1007/978-3-319-96812-4_16}
}

@inproceedings{RISC5713,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Generalization}},
booktitle = {{32nd International Workshop on Unification, UNIF 2018}},
language = {english},
pages = { -- },
isbn_issn = { },
year = {2018},
editor = {Mauricio Ayala-Rincon and Philippe Balbiani},
refereed = {yes},
length = {0}
}

@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}
}

@inproceedings{RISC5473,
author = {Mauricio Ayala-Rincon and Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Rewriting Logic from a ρLog Point of View}},
booktitle = {{Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017) }},
language = {english},
pages = {--},
isbn_issn = { },
year = {2017},
editor = {Sandra Alves and Renata Wasserman},
refereed = {yes},
length = {16}
}

@inproceedings{RISC5546,
author = {E. Abraham and T. Jebelean},
title = {{Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks}},
booktitle = {{ICAI 2017: 10th International Conference on Applied Informatics}},
language = {English},
abstract = {We develop a case study on using quantifier elimination and cylindrical algebraic decomposition for the purpose of finding specific terms for the automation of proving mathematical properties in elementary analysis.Real--life proofs in specific mathematical domains are difficult to automate because of the high number of assumptions necessary for the prover to succeed. In particular, in elementary analysis, it is allmost impossible to find automatically the appropriate terms for the instantiation of universal assumptions and for witnessing the existential goals. We aim at developing such proofs in natural style, in the frame of the{\em Theorema} system.Finding such terms is actually possible by using quantifier elimination (QE) based on cylindrical algebraic decomposition (CAD). However, the current straightforward approach lacks in efficiency, because several redundant calls may be necessary, and because the nature of the problem is slightly different.We study some natural--style proofs, the necessary special terms, and the corresponding usage of the QE/CAD, and identify specific techniques for adapting these algorithms in order to increase their efficiency.The experiments are performed partially in {\em Mathematica} and partially in {\tt SMT-RAT}, the latter used as ``white--box'', which allows to inspect the intermediate results and to adapt certain parts of the algorithms.},
pages = {0--0},
isbn_issn = {ISBN 0},
year = {2017},
note = {In print},
editor = {G. Kusper},
refereed = {yes},
length = {0},
conferencename = {ICAI 2017: 10th International Conference on Applied Informatics},
url = {https://icai.uni-eszterhazy.hu/}
}

@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}
}

@inproceedings{RISC4536,
author = {A. Maletzky and W. Windsteiger},
title = {{The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema}},
booktitle = {{Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10383},
pages = {25--39},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-62075-6},
year = {2017},
note = {doi 10.1007/978-3-319-62075-6_3},
editor = {H. Geuvers and M. England and O. Hasan and F. Rabe and O. Teschke},
refereed = {yes},
length = {15},
url = {https://link.springer.com/chapter/10.1007/978-3-319-62075-6_3}
}

@inproceedings{RISC5516,
author = {W. Windsteiger},
title = {{Theorema 2.0: A Brief Tutorial}},
booktitle = {{Proceedings of SYNASC 2017}},
language = {english},
abstract = {The Theorema system aims to be a computer assistant for theworking mathematician. Support should be given throughout all phases ofmathematical activity, from introducing new mathematical concepts bydefinitions or axioms, through first (computational) experiments, theformulation of theorems, their justification by an exact proof, theapplication of a theorem as an algorithm, to the dissemination of theresults in form of a mathematical publication, the build up of biggerlibraries of certified mathematical content and the like. One focus lieson the natural style of system input (in form of definitions, theorems,algorithms, etc.), system output (mainly in formof mathematical proofs) and user interaction. When using the Theoremasystem, a user should not have to follow a certain style of mathematicsenforced by the system (e.g. basing all of mathematics on set theory orcertain variants of type theory), rather should the system support theuser in her preferred flavor of doing math. The new implementation ofthe system, which we refer to as Theorema 2.0, is open-source andavailable through GitHub.},
series = {IEEE Explore},
pages = {1--3},
isbn_issn = {?},
year = {2017},
editor = {Tudor Jebelean and Daniela Zaharie},
refereed = {yes},
length = {3},
conferencename = {SYNASC 2017}
}

@inproceedings{RISC5324,
author = {Bruno Buchberger},
title = {{Stam's Identities Collection: A Case Study for Math Knowledge Bases}},
booktitle = {{Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings}},
language = {english},
pages = {437--442},
publisher = {Springer International Publishing},
address = {Cham},
isbn_issn = {978-3-319-42432-3},
year = {2016},
editor = {Gert-Martin Greuel and Thorsten Koch and Peter Paule and Andrew Sommese},
refereed = {no},
length = {6},
url = {http://dx.doi.org/10.1007/978-3-319-42432-3_55}
}

@inproceedings{RISC5325,
author = {Bruno Buchberger},
title = {{The GDML and EuKIM Projects: Short Report on the Initiative}},
booktitle = {{Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings}},
language = {english},
pages = {443--446},
publisher = {Springer International Publishing},
address = {Cham},
isbn_issn = {978-3-319-42432-3},
year = {2016},
editor = {Gert-Martin Greuel and Thorsten Koch and Peter Paule and Andrew Sommese},
refereed = {no},
length = {4},
url = {http://dx.doi.org/10.1007/978-3-319-42432-3_56}
}

@inproceedings{RISC5198,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Proof-based Synthesis of Sorting Algorithms for Trees}},
booktitle = {{Proceedings of LATA 2016, the 10th International Conference on Language and Automata Theory and Applications}},
language = {english},
series = {LNCS},
volume = {9618},
pages = {562--575},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-29999-0},
year = {2016},
editor = {Adrian-Horia Dediu and Jan Janousek and Carlos Martin-Vide and Bianca Truthe},
refereed = {yes},
length = {14},
conferencename = {LATA 2016}
}