Generalization ALgorithms and Applications [GALA]
Project Lead
Project Duration
01/02/2016 - 31/01/2021Project URL
Go to Website
Partners
The Austrian Science Fund (FWF)
Publications
2019
[Cerna]
A Generic Framework for Higher-Order Generalizations
David M. Cerna, Temur Kutsia
Technical report no. 19-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]@techreport{RISC5883,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
language = {english},
number = {19-01},
year = {2019},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
language = {english},
number = {19-01},
year = {2019},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]
Higher-Order Pattern Generalization Modulo Equational Theories
David M. Cerna and Temur Kutsia
2019. [pdf]@techreport{RISC5918,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
language = {english},
abstract = {We consider anti-unification for simply typed lambda terms in theories defined by associativity,commutativity, identity (unit element) axioms and their combinations, and develop a sound andcomplete algorithm which takes two lambda terms and computes their equational generalizations inthe form of higher-order patterns. The problem is finitary: the minimal complete set of suchgeneralizations contains finitely many elements. We define the notion of optimal solution andinvestigate special fragments of the problem for which the optimal solution can be computed in linearor polynomial time.},
year = {2019},
length = {25},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
language = {english},
abstract = {We consider anti-unification for simply typed lambda terms in theories defined by associativity,commutativity, identity (unit element) axioms and their combinations, and develop a sound andcomplete algorithm which takes two lambda terms and computes their equational generalizations inthe form of higher-order patterns. The problem is finitary: the minimal complete set of suchgeneralizations contains finitely many elements. We define the notion of optimal solution andinvestigate special fragments of the problem for which the optimal solution can be computed in linearor polynomial time.},
year = {2019},
length = {25},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
2018
[Amiridze]
Anti-Unification and Natural Language Processing
N. Amiridze, T. Kutsia
In: Fifth Workshop on Natural Language and Computer Science, NLCS’18, A. Asudeh, V. de Paiva, L. Moss (ed.), EasyChair preprints 203, pp. 1-12. 2018. [url] [pdf]@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}
}
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}
}
[Baumgartner]
Term-Graph Anti-Unification
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret
Technical report no. 18-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2018. [pdf]@techreport{RISC5549,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
language = {english},
number = {18-02},
year = {2018},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
language = {english},
number = {18-02},
year = {2018},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]
Primitive Recursive Proof Systems for Arithmetic
David M. Cerna
RISC. Technical report, January 2018. In revision. [pdf]@techreport{RISC5528,
author = {David M. Cerna},
title = {{Primitive Recursive Proof Systems for Arithmetic}},
language = {english},
abstract = {Peano arithmetic, as formalized by Gentzen, can be presented as an axiom extensionof the LK-calculus with equality and an additional inference rule formalizing induction.While this formalism was enough (with the addition of some meta-theoretic argumentation)to show the consistency of arithmetic, alternative formulations of induction such asthe infinitary ω-rule and cyclic reasoning provide insight into the structure of arithmeticproofs obfuscated by the inference rule formulation of induction. For example, questionsconcerning the elimination of cut, consistency, and proof shape are given more clarity. Thesame could be said for functional interpretations of arithmetic such as system T whichenumerates the recursive functions provably total by arithmetic. A key feature of thesevariations on the formalization of arithmetic is that they get somewhat closer to formalizingthe concept of induction directly using the inferences of the LK-calculus, albeit byadding extra machinery at the meta-level. In this work we present a recursive sequentcalculus for arithmetic which can be syntactically translated into Gentzen formalism ofarithmetic and allows proof normalization to the LK-calculus with equality.},
year = {2018},
month = {January },
note = {In revision},
institution = {RISC},
length = {20}
}
author = {David M. Cerna},
title = {{Primitive Recursive Proof Systems for Arithmetic}},
language = {english},
abstract = {Peano arithmetic, as formalized by Gentzen, can be presented as an axiom extensionof the LK-calculus with equality and an additional inference rule formalizing induction.While this formalism was enough (with the addition of some meta-theoretic argumentation)to show the consistency of arithmetic, alternative formulations of induction such asthe infinitary ω-rule and cyclic reasoning provide insight into the structure of arithmeticproofs obfuscated by the inference rule formulation of induction. For example, questionsconcerning the elimination of cut, consistency, and proof shape are given more clarity. Thesame could be said for functional interpretations of arithmetic such as system T whichenumerates the recursive functions provably total by arithmetic. A key feature of thesevariations on the formalization of arithmetic is that they get somewhat closer to formalizingthe concept of induction directly using the inferences of the LK-calculus, albeit byadding extra machinery at the meta-level. In this work we present a recursive sequentcalculus for arithmetic which can be syntactically translated into Gentzen formalism ofarithmetic and allows proof normalization to the LK-calculus with equality.},
year = {2018},
month = {January },
note = {In revision},
institution = {RISC},
length = {20}
}
[Cerna]
A General Recursive Construction for Schematic Resolution Derivations
David M. Cerna
2018. submitted for review. Preprint. [pdf]@techreport{RISC5594,
author = {David M. Cerna},
title = {{A General Recursive Construction for Schematic Resolution Derivations}},
language = {english},
abstract = {Proof schemata provide an alternative formalism for handling inductive argumentation, while non-trivially extending {\em Herbrand's theorem} to a fragment of arithmetic and thus allowing the construction of {\em Herbrand sequents} and {\em expansion trees}. Existing proof analysis methods for proof schemata extract an unsatisfiable characteristic formula representing the cut structure of the proof and from its refutation construct a Herbrand sequent. Unfortunately, constructing the refutation is a task which is highly non-trivial. An automated method for constructing such refutations exists, but it only works for a very weak fragment of arithmetic and is hard to use interactively. More expressive yet interactive methods for the formalization of recursive resolution refutation are complex, hard to work with, and still limited to an undesirably weak class of recursion. In this work we note a particular problem with previous methods, namely they mix the recursive structure with the calculus of refutation. Also we present a modular recursive structure independent of the resolution formalism and proof construction. We illustrate the expressive power of the so called {\em finite saturated tree} formalism by formalizing the Non-injectivity Assertion's schematic refutation (a variant of the infinitary Pigeonhole principle). None of the previously developed formalism are able to formalize this refutation.},
year = {2018},
note = {submitted for review},
length = {42},
type = {Preprint},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
author = {David M. Cerna},
title = {{A General Recursive Construction for Schematic Resolution Derivations}},
language = {english},
abstract = {Proof schemata provide an alternative formalism for handling inductive argumentation, while non-trivially extending {\em Herbrand's theorem} to a fragment of arithmetic and thus allowing the construction of {\em Herbrand sequents} and {\em expansion trees}. Existing proof analysis methods for proof schemata extract an unsatisfiable characteristic formula representing the cut structure of the proof and from its refutation construct a Herbrand sequent. Unfortunately, constructing the refutation is a task which is highly non-trivial. An automated method for constructing such refutations exists, but it only works for a very weak fragment of arithmetic and is hard to use interactively. More expressive yet interactive methods for the formalization of recursive resolution refutation are complex, hard to work with, and still limited to an undesirably weak class of recursion. In this work we note a particular problem with previous methods, namely they mix the recursive structure with the calculus of refutation. Also we present a modular recursive structure independent of the resolution formalism and proof construction. We illustrate the expressive power of the so called {\em finite saturated tree} formalism by formalizing the Non-injectivity Assertion's schematic refutation (a variant of the infinitary Pigeonhole principle). None of the previously developed formalism are able to formalize this refutation.},
year = {2018},
note = {submitted for review},
length = {42},
type = {Preprint},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Dundua]
Pattern-based calculi with finitary matching
Sandra Alves, Besik Dundua, Mário Florido, Temur Kutsia
Logic Journal of the IGPL 26(2), pp. 203-243. 2018. ISSN 1367-0751. [url]@article{RISC5763,
author = {Sandra Alves and Besik Dundua and Mário Florido and Temur Kutsia},
title = {{Pattern-based calculi with finitary matching}},
language = {english},
journal = {Logic Journal of the IGPL},
volume = {26},
number = {2},
pages = {203--243},
isbn_issn = {ISSN 1367-0751},
year = {2018},
refereed = {yes},
length = {41},
url = {https://doi.org/10.1093/JIGPAL/jzx059}
}
author = {Sandra Alves and Besik Dundua and Mário Florido and Temur Kutsia},
title = {{Pattern-based calculi with finitary matching}},
language = {english},
journal = {Logic Journal of the IGPL},
volume = {26},
number = {2},
pages = {203--243},
isbn_issn = {ISSN 1367-0751},
year = {2018},
refereed = {yes},
length = {41},
url = {https://doi.org/10.1093/JIGPAL/jzx059}
}
[Kutsia]
Idempotent Generalization is Infinitary
David M. Cerna and Temur Kutsia
RISC. Technical report, RISC Report, 2018. [pdf]@techreport{RISC5529,
author = {David M. Cerna and Temur Kutsia},
title = {{Idempotent Generalization is Infinitary}},
language = {english},
abstract = {Let §\mathbf{I}_{S}$ be an equational theory s.t. for each $f\in S$, $f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP) $f(a,b) \triangleq g(a,b)$ modulo $\mathbf{I}_{\lbrace f,g \rbrace}$ admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo $\mathbf{I}_{\lbrace f\rbrace}$, $f(a,f(a,b)) \triangleq f(b,f(a,b))$ admits infinitely many lggs.},
year = {2018},
howpublished = {RISC Report},
institution = {RISC},
length = {1}
}
author = {David M. Cerna and Temur Kutsia},
title = {{Idempotent Generalization is Infinitary}},
language = {english},
abstract = {Let §\mathbf{I}_{S}$ be an equational theory s.t. for each $f\in S$, $f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP) $f(a,b) \triangleq g(a,b)$ modulo $\mathbf{I}_{\lbrace f,g \rbrace}$ admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo $\mathbf{I}_{\lbrace f\rbrace}$, $f(a,f(a,b)) \triangleq f(b,f(a,b))$ admits infinitely many lggs.},
year = {2018},
howpublished = {RISC Report},
institution = {RISC},
length = {1}
}
[Pau]
Proximity-Based Generalization
Temur Kutsia, Cleo Pau
In: 32nd International Workshop on Unification, UNIF 2018, Mauricio Ayala-Rincon and Philippe Balbiani (ed.), pp. - . 2018. [pdf]@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}
}
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}
}
2017
[Cerna]
Integrating a Global Induction Mechanism into a Sequent Calculus
David M. Cerna and Michael Lettmann
In: TABLEAUX 2017, Renate A. Schmidt and Cl{\'{a}}udia Nalon (ed.), Proceedings of Tableaux, lecture notes in computer science , pp. 278-294. September 2017. Springer, 978-3-319-66901-4.@inproceedings{RISC5471,
author = {David M. Cerna and Michael Lettmann},
title = {{Integrating a Global Induction Mechanism into a Sequent Calculus}},
booktitle = {{TABLEAUX 2017}},
language = {english},
abstract = {Most interesting proofs in mathematics contain an inductive argument which requires an extension of the \textbf{LK}-calculus to formalize. The mostcommonly used calculi contain a separate rule or axiom which reduces the important proof theoretic properties of the calculus. In such cases cut-elimination does not result in analytic proofs, i.e.\ every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a generalization of \textbf{LK}-proofs able to simulate induction by linking proofs, indexed by a natural number, together.Using a global cut-elimination method a normal form can be reached which allows a schema of {\em Herbrand Sequents} to be produced, an essential step for proof analysis in the presence ofinduction. However, proof schema have only been studied in a limited context and are currentlydefined for a very particular proof structure based on a slight extension of the \textbf{LK}-calculus. The result is an opaque and complex formalization. In this paper, we introduce a calculus integrating the proof schema formalization and in the process we elucidate properties of proof schemata which can be used to extend the formalism. },
series = {lecture notes in computer science},
pages = {278--294},
publisher = {Springer},
isbn_issn = {978-3-319-66901-4},
year = {2017},
month = {September},
editor = {Renate A. Schmidt and Cl{\'{a}}udia Nalon},
refereed = {yes},
length = {16},
conferencename = {Tableaux}
}
author = {David M. Cerna and Michael Lettmann},
title = {{Integrating a Global Induction Mechanism into a Sequent Calculus}},
booktitle = {{TABLEAUX 2017}},
language = {english},
abstract = {Most interesting proofs in mathematics contain an inductive argument which requires an extension of the \textbf{LK}-calculus to formalize. The mostcommonly used calculi contain a separate rule or axiom which reduces the important proof theoretic properties of the calculus. In such cases cut-elimination does not result in analytic proofs, i.e.\ every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a generalization of \textbf{LK}-proofs able to simulate induction by linking proofs, indexed by a natural number, together.Using a global cut-elimination method a normal form can be reached which allows a schema of {\em Herbrand Sequents} to be produced, an essential step for proof analysis in the presence ofinduction. However, proof schema have only been studied in a limited context and are currentlydefined for a very particular proof structure based on a slight extension of the \textbf{LK}-calculus. The result is an opaque and complex formalization. In this paper, we introduce a calculus integrating the proof schema formalization and in the process we elucidate properties of proof schemata which can be used to extend the formalism. },
series = {lecture notes in computer science},
pages = {278--294},
publisher = {Springer},
isbn_issn = {978-3-319-66901-4},
year = {2017},
month = {September},
editor = {Renate A. Schmidt and Cl{\'{a}}udia Nalon},
refereed = {yes},
length = {16},
conferencename = {Tableaux}
}
[Cerna]
Towards a Clausal Analysis of Proof Schemata
David M. Cerna and Michael Lettmann
In: SYNASC 2017, Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephan Watt (ed.), IEEE Xplore , pp. 113-120. September 2017. 978-1-5386-2625-2.@inproceedings{RISC5472,
author = {David M. Cerna and Michael Lettmann},
title = {{Towards a Clausal Analysis of Proof Schemata}},
booktitle = {{SYNASC 2017}},
language = {english},
abstract = {Proof schemata are a variant of \LK-proofs able to simulate various induction schemes in first-order logic by adding so called {\em links} to the standard first-order \LK-calculus. Links allow proofs to reference other proofs, and thus give schemata a recursive structure. {\em Gentzen} style cut-elimination methods, which reduce cuts locally, does not work in the presence of links. However, an alternative method, such as cut-elimination by resolution (CERES), which eliminate cuts globally, is able to reduce cuts over the entire recursive structure simultaneously. Unfortunately, analysis of the cut structure of a proof after partial cut-elimination is non-trivial. By extending local methods to proof schemata, we provide such an analysis. },
series = {IEEE Xplore},
pages = {113--120},
isbn_issn = {978-1-5386-2625-2},
year = {2017},
month = {September},
editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephan Watt},
refereed = {yes},
length = {8}
}
author = {David M. Cerna and Michael Lettmann},
title = {{Towards a Clausal Analysis of Proof Schemata}},
booktitle = {{SYNASC 2017}},
language = {english},
abstract = {Proof schemata are a variant of \LK-proofs able to simulate various induction schemes in first-order logic by adding so called {\em links} to the standard first-order \LK-calculus. Links allow proofs to reference other proofs, and thus give schemata a recursive structure. {\em Gentzen} style cut-elimination methods, which reduce cuts locally, does not work in the presence of links. However, an alternative method, such as cut-elimination by resolution (CERES), which eliminate cuts globally, is able to reduce cuts over the entire recursive structure simultaneously. Unfortunately, analysis of the cut structure of a proof after partial cut-elimination is non-trivial. By extending local methods to proof schemata, we provide such an analysis. },
series = {IEEE Xplore},
pages = {113--120},
isbn_issn = {978-1-5386-2625-2},
year = {2017},
month = {September},
editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephan Watt},
refereed = {yes},
length = {8}
}
[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]@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}
}
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]
Rewriting Logic from a ρLog Point of View
Mauricio Ayala-Rincon, Besik Dundua, Temur Kutsia, Mircea Marin
In: Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017) , Sandra Alves and Renata Wasserman (ed.), pp. -. 2017. [pdf]@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}
}
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}
}
[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. [url]@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}
}
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]
Mathematical Aspects of Computer and Information Sciences
Johannes Blömer, Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos, editors
Lecture Notes in Computer Science 10693, 2017. Springer, ISBN 978-3-319-72452-2. [url]@booklet{RISC5518,
author = {Johannes Blömer and Ilias Kotsireas and Temur Kutsia and Dimitris E. Simos and editors},
title = {{Mathematical Aspects of Computer and Information Sciences}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10693},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-72452-2},
year = {2017},
edition = { },
translation = {0},
length = {462},
url = {https://doi.org/10.1007/978-3-319-72453-9}
}
author = {Johannes Blömer and Ilias Kotsireas and Temur Kutsia and Dimitris E. Simos and editors},
title = {{Mathematical Aspects of Computer and Information Sciences}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10693},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-72452-2},
year = {2017},
edition = { },
translation = {0},
length = {462},
url = {https://doi.org/10.1007/978-3-319-72453-9}
}
2016
[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]@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}
}
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, Schloss Hagenberg, 4232 Hagenberg, Austria. 2016. [pdf]@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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[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]@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}
}
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]@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}
}
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, Schloss Hagenberg, 4232 Hagenberg, Austria. 2016. [pdf]@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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
