Software
PρLog (pronounced Pē-rō-log) is an experimental tool that extends logic programming with strategic conditional transformation rules, combining Prolog with ρLog calculus. It deals with term sequences (also called hedges), transforming them by conditional rules. Transformations are nondeterministic and may yield ...
Authors: Teimuraz Kutsia, Mircea Marin
MoreSoftware WebsiteThis 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 ...
Publications
2021
[Cerna]
A Special Case of Schematic Syntactic Unification
David M. Cerna
CAS ICS / RISC. Technical report, 2021. [pdf]@techreport{RISC6349,
author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}
author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}
[Dundua]
Variadic equational matching in associative and commutative theories
Besik Dundua, Temur Kutsia, Mircea Marin
Journal of Symbolic Computation 106, pp. 78-109. 2021. Elsevier, ISSN 0747-7171. [doi] [pdf]@article{RISC6260,
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic equational matching in associative and commutative theories}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {106},
pages = {78--109},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1016/j.jsc.2021.01.001}
}
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic equational matching in associative and commutative theories}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {106},
pages = {78--109},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1016/j.jsc.2021.01.001}
}
[Pau]
Proximity-Based Unification and Matching for Full Fuzzy Signatures
Temur Kutsia, Cleo Pau
Technical report no. 21-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]@techreport{RISC6296,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},
language = {english},
abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},
number = {21-08},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},
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)}
}
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},
language = {english},
abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},
number = {21-08},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},
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)}
}
[Pau]
Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures
Temur Kutsia, Cleo Pau
Technical report no. 21-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]@techreport{RISC6297,
author = {Temur Kutsia and Cleo Pau},
title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},
number = {21-09},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},
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)}
}
author = {Temur Kutsia and Cleo Pau},
title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},
number = {21-09},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},
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)}
}
2020
[Cerna]
Idempotent Anti-unification
David Cerna, Temur Kutsia
ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2020. ACM Press, ISSN 1529-3785. [doi] [pdf]@article{RISC6023,
author = {David Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification}},
language = {english},
journal = {ACM Transactions on Computational Logic (TOCL)},
volume = {21},
number = {2},
pages = {10:1--10:32},
publisher = {ACM Press},
isbn_issn = {ISSN 1529-3785},
year = {2020},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
author = {David Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification}},
language = {english},
journal = {ACM Transactions on Computational Logic (TOCL)},
volume = {21},
number = {2},
pages = {10:1--10:32},
publisher = {ACM Press},
isbn_issn = {ISSN 1529-3785},
year = {2020},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Cerna]
Unital Anti-Unification: Type and Algorithms
David M. Cerna, Temur Kutsia
In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 26:1-26:20. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [url]@inproceedings{RISC6132,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {26:1--26:20},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {20},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12352/}
}
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {26:1--26:20},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {20},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12352/}
}
[Cerna]
Higher-order pattern generalization modulo equational theories
David M. Cerna, Temur Kutsia
Mathematical Structures in Computer Science 30(6), pp. 627-663. 2020. ISSN 0960-1295. [url]@article{RISC6226,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-order pattern generalization modulo equational theories}},
language = {english},
journal = {Mathematical Structures in Computer Science},
volume = {30},
number = {6},
pages = {627--663},
isbn_issn = {ISSN 0960-1295},
year = {2020},
refereed = {yes},
length = {37},
url = {https://www.cambridge.org/core/services/aop-cambridge-core/content/view/88E26F155F0FD02B3EDD648971D9AD1B/S0960129520000110a.pdf/higher-order-pattern-generalization-modulo-equational-theories.pdf}
}
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-order pattern generalization modulo equational theories}},
language = {english},
journal = {Mathematical Structures in Computer Science},
volume = {30},
number = {6},
pages = {627--663},
isbn_issn = {ISSN 0960-1295},
year = {2020},
refereed = {yes},
length = {37},
url = {https://www.cambridge.org/core/services/aop-cambridge-core/content/view/88E26F155F0FD02B3EDD648971D9AD1B/S0960129520000110a.pdf/higher-order-pattern-generalization-modulo-equational-theories.pdf}
}
[Cerna]
Anti-unification and the Theory of Semirings
David M. Cerna
Theor. Comput. Sci. 848, pp. 133-139. 2020. RISC / CAS ICS, 0304-3975. [doi]@article{RISC6234,
author = {David M. Cerna},
title = {{Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only unitequations (more than one) is nullary. Such pure theories are artificial and are of little effect onpractical aspects of anti-unification. In this work, we extend these nullarity results to the theory ofsemirings, a heavily studied theory with many practical applications. Furthermore, our argumentholds over semirings with commutative multiplication and/or idempotent addition. We also cover afew open questions discussed in previous work.},
journal = {Theor. Comput. Sci.},
volume = {848},
pages = {133--139},
isbn_issn = {0304-3975},
year = {2020},
refereed = {yes},
institution = {RISC / CAS ICS},
length = {7},
url = {https://doi.org/10.1016/j.tcs.2020.10.020}
}
author = {David M. Cerna},
title = {{Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only unitequations (more than one) is nullary. Such pure theories are artificial and are of little effect onpractical aspects of anti-unification. In this work, we extend these nullarity results to the theory ofsemirings, a heavily studied theory with many practical applications. Furthermore, our argumentholds over semirings with commutative multiplication and/or idempotent addition. We also cover afew open questions discussed in previous work.},
journal = {Theor. Comput. Sci.},
volume = {848},
pages = {133--139},
isbn_issn = {0304-3975},
year = {2020},
refereed = {yes},
institution = {RISC / CAS ICS},
length = {7},
url = {https://doi.org/10.1016/j.tcs.2020.10.020}
}
[Cerna]
Schematic Refutations of Formula Schemata
David Cerna and Alexander Leitsch and Anela Lolic
Journal of Automated Reasoning, pp. -. 2020. 1573-0670. [doi]@article{RISC6235,
author = {David Cerna and Alexander Leitsch and Anela Lolic},
title = {{Schematic Refutations of Formula Schemata}},
language = {english},
abstract = {Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.},
journal = {Journal of Automated Reasoning},
pages = {--},
isbn_issn = {1573-0670},
year = {2020},
refereed = {yes},
length = {47},
url = {https://doi.org/10.1007/s10817-020-09583-8}
}
author = {David Cerna and Alexander Leitsch and Anela Lolic},
title = {{Schematic Refutations of Formula Schemata}},
language = {english},
abstract = {Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.},
journal = {Journal of Automated Reasoning},
pages = {--},
isbn_issn = {1573-0670},
year = {2020},
refereed = {yes},
length = {47},
url = {https://doi.org/10.1007/s10817-020-09583-8}
}
[Cerna]
A Mobile Application for Self-Guided Study of Formal Reasoning
David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya
In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019, Pedro Quaresma and Walther Neuper and Jo{ {a}}o Marcos (ed.), EPTCS 313, pp. 35-53. 2020. 2075-2180. [doi]@inproceedings{RISC6236,
author = {David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya},
title = {{A Mobile Application for Self-Guided Study of Formal Reasoning}},
booktitle = {{Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019}},
language = {english},
abstract = {In this work, we introduce AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Unlike most of the existing study aids for formal reasoning, AXolotl is an Android-based application with a simple touch-based interface. Part of the design goal was to minimize the possibility of user errors which distract from the learning process. Such as typos or inconsistent application of the provided rules. The system includes a zoomable proof viewer which displays the progress made so far and allows for storage of the completed proofs as a JPEG or LaTeX file. The software is available on the google play store and comes with a small library of problems. Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotl supports problems that can be solved using rules which transform a single expression into a set of expressions. This covers educational scenarios found in our first-semester introduction to logic course and helps bridge the gap between propositional and first-order reasoning. Future developments will include rewrite rules which take a set of expressions and return a set of expressions, as well as a quantified first-order extension.},
series = {EPTCS},
volume = {313},
pages = {35--53},
isbn_issn = {2075-2180},
year = {2020},
editor = {Pedro Quaresma and Walther Neuper and Jo{~{a}}o Marcos},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4204/EPTCS.313.3}
}
author = {David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya},
title = {{A Mobile Application for Self-Guided Study of Formal Reasoning}},
booktitle = {{Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019}},
language = {english},
abstract = {In this work, we introduce AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Unlike most of the existing study aids for formal reasoning, AXolotl is an Android-based application with a simple touch-based interface. Part of the design goal was to minimize the possibility of user errors which distract from the learning process. Such as typos or inconsistent application of the provided rules. The system includes a zoomable proof viewer which displays the progress made so far and allows for storage of the completed proofs as a JPEG or LaTeX file. The software is available on the google play store and comes with a small library of problems. Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotl supports problems that can be solved using rules which transform a single expression into a set of expressions. This covers educational scenarios found in our first-semester introduction to logic course and helps bridge the gap between propositional and first-order reasoning. Future developments will include rewrite rules which take a set of expressions and return a set of expressions, as well as a quantified first-order extension.},
series = {EPTCS},
volume = {313},
pages = {35--53},
isbn_issn = {2075-2180},
year = {2020},
editor = {Pedro Quaresma and Walther Neuper and Jo{~{a}}o Marcos},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4204/EPTCS.313.3}
}
[Cerna]
Unital Anti-Unification: Type and Algorithms
David M. Cerna , Temur Kutsia
In: 5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference, Zena M. Ariola (ed.), Proceedings of FSCD, LIPICS 16720-02, pp. 1-20. 2020. 1868-8969. [doi]@inproceedings{RISC6237,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference}},
language = {english},
abstract = {Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions. },
series = {LIPICS},
volume = {167},
number = {20-02},
pages = {1--20},
isbn_issn = {1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
conferencename = {FSCD},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.26}
}
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference}},
language = {english},
abstract = {Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions. },
series = {LIPICS},
volume = {167},
number = {20-02},
pages = {1--20},
isbn_issn = {1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
conferencename = {FSCD},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.26}
}
[Dramnesc]
Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema
Isabela Dramnesc, Tudor Jebelean
Technical report no. 20-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2020. [pdf]@techreport{RISC6094,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema}},
language = {english},
number = {20-04},
year = {2020},
month = {April},
length = {25},
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)}
}
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema}},
language = {english},
number = {20-04},
year = {2020},
month = {April},
length = {25},
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)}
}
[Dramnesc]
Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema
Isabela Dramnesc, Tudor Jebelean
Technical report no. 20-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). September 2020. [pdf]@techreport{RISC6206,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema}},
language = {English},
abstract = {We demonstrate the deduction based synthesis of element deletion algorithms for[sorted] lists and [sorted] binary trees, by first developing the necessary theory which ismulti–type: basic ordered elements, multisets, lists, and trees. The generated algorithms are“pattern matching”, namely sets of conditional equalities, and we also demonstrate theirtransformation into functional algorithms and, for lists, into tail recursive algorithms. Thiswork constitutes a case study first in theory exploration and second in automated synthesisand transformation of algorithms synthesized on the basis of natural style proofs, whichallows to investigate the heuristics of theory construction on multiple types, as well as thenatural style inferences and strategies for constructing human readable synthesis proofs. Theexperiments are performed in the frame of the Theorema system.},
number = {20-15},
year = {2020},
month = {September},
keywords = {automated reasoning; algorithm synthesis; lists; binary trees; multisets; Theorema},
length = {22},
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)}
}
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema}},
language = {English},
abstract = {We demonstrate the deduction based synthesis of element deletion algorithms for[sorted] lists and [sorted] binary trees, by first developing the necessary theory which ismulti–type: basic ordered elements, multisets, lists, and trees. The generated algorithms are“pattern matching”, namely sets of conditional equalities, and we also demonstrate theirtransformation into functional algorithms and, for lists, into tail recursive algorithms. Thiswork constitutes a case study first in theory exploration and second in automated synthesisand transformation of algorithms synthesized on the basis of natural style proofs, whichallows to investigate the heuristics of theory construction on multiple types, as well as thenatural style inferences and strategies for constructing human readable synthesis proofs. Theexperiments are performed in the frame of the Theorema system.},
number = {20-15},
year = {2020},
month = {September},
keywords = {automated reasoning; algorithm synthesis; lists; binary trees; multisets; Theorema},
length = {22},
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]
Constraint Solving over Multiple Similarity Relations
Besik Dundua, Temur Kutsia, Mircea Marin, Cleopatra Pau
In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 30:1-30:19. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [doi]@inproceedings{RISC6133,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleopatra Pau},
title = {{Constraint Solving over Multiple Similarity Relations}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {30:1--30:19},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.30}
}
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleopatra Pau},
title = {{Constraint Solving over Multiple Similarity Relations}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {30:1--30:19},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.30}
}
[Dundua]
Extending the 𝜌Log Calculus with Proximity Relations
Besik Dundua, Temur Kutsia, Mircea Marin, Cleo Pau
In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 83-100. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [doi] [pdf]@incollection{RISC6227,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleo Pau},
title = {{Extending the 𝜌Log Calculus with Proximity Relations}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {83--100},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-56356-1_6}
}
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleo Pau},
title = {{Extending the 𝜌Log Calculus with Proximity Relations}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {83--100},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-56356-1_6}
}
[Dundua]
Specification and Analysis of ABAC Policies in a Rule-Based Framework
Besik Dundua, Temur Kutsia, Mircea Marin, Mikheil Rukhaia
In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 101-116. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [doi] [pdf]@incollection{RISC6228,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Mikheil Rukhaia},
title = {{Specification and Analysis of ABAC Policies in a Rule-Based Framework}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {101--116},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {16},
url = {https://doi.org/10.1007/978-3-030-56356-1_7}
}
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Mikheil Rukhaia},
title = {{Specification and Analysis of ABAC Policies in a Rule-Based Framework}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {101--116},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {16},
url = {https://doi.org/10.1007/978-3-030-56356-1_7}
}
[Dundua]
A Rule-Based System for Computation and Deduction in Mathematica
Mircea Marin, Besik Dundua, Temur Kutsia
In: WRLA 2020: Rewriting Logic and Its Applications, Santiago Escobar, Narciso Martí-Oliet (ed.), Lecture Notes in Computer Science 12328, pp. 57-74. 2020. Springer, ISBN 978-3-030-63595-4, 978-3-030-63594-7. [doi] [pdf]@inproceedings{RISC6229,
author = {Mircea Marin and Besik Dundua and Temur Kutsia},
title = {{A Rule-Based System for Computation and Deduction in Mathematica}},
booktitle = {{WRLA 2020: Rewriting Logic and Its Applications}},
language = {english},
series = { Lecture Notes in Computer Science},
volume = {12328},
pages = {57--74},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-63595-4, 978-3-030-63594-7},
year = {2020},
editor = {Santiago Escobar and Narciso Martí-Oliet},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-63595-4_4}
}
author = {Mircea Marin and Besik Dundua and Temur Kutsia},
title = {{A Rule-Based System for Computation and Deduction in Mathematica}},
booktitle = {{WRLA 2020: Rewriting Logic and Its Applications}},
language = {english},
series = { Lecture Notes in Computer Science},
volume = {12328},
pages = {57--74},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-63595-4, 978-3-030-63594-7},
year = {2020},
editor = {Santiago Escobar and Narciso Martí-Oliet},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-63595-4_4}
}
[Dundua]
Unranked Nominal Unification
Besik Dundua, Temur Kutsia, Mikheil Rukhaia
Technical report no. 20-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2020. [pdf]@techreport{RISC6273,
author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},
title = {{Unranked Nominal Unification}},
language = {english},
number = {20-21},
year = {2020},
sponsor = {FWF, project 28789-N32},
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)}
}
author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},
title = {{Unranked Nominal Unification}},
language = {english},
number = {20-21},
year = {2020},
sponsor = {FWF, project 28789-N32},
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)}
}
[Kutsia]
Unification modulo alpha-equivalence in a mathematical assistant system
Temur Kutsia
Technical report no. 20-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2020. [pdf]@techreport{RISC6074,
author = {Temur Kutsia},
title = {{Unification modulo alpha-equivalence in a mathematical assistant system}},
language = {english},
number = {20-01},
year = {2020},
length = {21},
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)}
}
author = {Temur Kutsia},
title = {{Unification modulo alpha-equivalence in a mathematical assistant system}},
language = {english},
number = {20-01},
year = {2020},
length = {21},
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 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]@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}
}
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}
}
