Ongoing Projects
Combinatorics and Codes for Information Security [SBA-K1]
Project Lead: Teimuraz Kutsia
Generalization ALgorithms and Applications [GALA]
Project Lead: Teimuraz Kutsia
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
2019
[Cerna]
Higher-Order Pattern Generalization Modulo Equational Theories with a unit element
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 with a unit element}},
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 with a unit element}},
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}
}
[Cerna]
A Generic Framework for Higher-Order Generalizations
David M. Cerna, Temur Kutsia
In: Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Herman Geuvers (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 10:1-10:19. 2019. Schloss Dagstuhl, ISSN 1868-8969. [url]@inproceedings{RISC5947,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {131},
pages = {10:1--10:19},
publisher = {Schloss Dagstuhl},
isbn_issn = {ISSN 1868-8969},
year = {2019},
editor = {Herman Geuvers},
refereed = {yes},
length = {19},
url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}
}
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {131},
pages = {10:1--10:19},
publisher = {Schloss Dagstuhl},
isbn_issn = {ISSN 1868-8969},
year = {2019},
editor = {Herman Geuvers},
refereed = {yes},
length = {19},
url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}
}
[Cerna]
On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences
David M. Cerna
2019. [pdf]@techreport{RISC5981,
author = {David M. Cerna},
title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
language = {english},
abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},
year = {2019},
length = {17},
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 = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
language = {english},
abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},
year = {2019},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]
Idempotent Anti-unification
David Cerna, Temur Kutsia
ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2019. ACM Press, ISSN 1529-3785. [url] [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 = {2019},
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 = {2019},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Dundua]
Variadic Equational Matching
Besik Dundua, Temur Kutsia, Mircea Marin
In: Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen (ed.), Lecture Notes in Computer Science 11617, pp. 77-92. 2019. Springer, ISBN 978-3-030-23249-8. [pdf]@inproceedings{RISC5948,
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic Equational Matching}},
booktitle = {{Intelligent Computer Mathematics - 12th International Conference, CICM 2019}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {11617},
pages = {77--92},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-23249-8},
year = {2019},
editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti Coen},
refereed = {yes},
length = {16}
}
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic Equational Matching}},
booktitle = {{Intelligent Computer Mathematics - 12th International Conference, CICM 2019}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {11617},
pages = {77--92},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-23249-8},
year = {2019},
editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti Coen},
refereed = {yes},
length = {16}
}
[Dundua]
A Rule-based Approach to the Decidability of Safety of ABACα
Mircea Marin, Temur Kutsia, Besik Dundua
In: Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019, Florian Kerschbaum, Atefeh Mashatan, Jianwei Niu, Adam J. Lee (ed.), pp. 173-178. 2019. ACM, ISBN 978-1-4503-6753-0. [url] [pdf]@inproceedings{RISC5955,
author = {Mircea Marin and Temur Kutsia and Besik Dundua},
title = {{A Rule-based Approach to the Decidability of Safety of ABACα}},
booktitle = {{Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019}},
language = {english},
pages = {173--178},
publisher = {ACM},
isbn_issn = {ISBN 978-1-4503-6753-0},
year = {2019},
editor = {Florian Kerschbaum and Atefeh Mashatan and Jianwei Niu and Adam J. Lee},
refereed = {yes},
length = {6},
url = {https://doi.org/10.1145/3322431.3325416}
}
author = {Mircea Marin and Temur Kutsia and Besik Dundua},
title = {{A Rule-based Approach to the Decidability of Safety of ABACα}},
booktitle = {{Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019}},
language = {english},
pages = {173--178},
publisher = {ACM},
isbn_issn = {ISBN 978-1-4503-6753-0},
year = {2019},
editor = {Florian Kerschbaum and Atefeh Mashatan and Jianwei Niu and Adam J. Lee},
refereed = {yes},
length = {6},
url = {https://doi.org/10.1145/3322431.3325416}
}
[Pau]
Computing All Maximal Clique Partitions in a Graph
Temur Kutsia, Cleo Pau
Technical report no. 19-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]@techreport{RISC5939,
author = {Temur Kutsia and Cleo Pau},
title = {{Computing All Maximal Clique Partitions in a Graph}},
language = {english},
number = {19-04},
year = {2019},
length = {9},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
author = {Temur Kutsia and Cleo Pau},
title = {{Computing All Maximal Clique Partitions in a Graph}},
language = {english},
number = {19-04},
year = {2019},
length = {9},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Pau]
Solving Proximity Constraints
Temur Kutsia, Cleo Pau
Technical report no. 19-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]@techreport{RISC5950,
author = {Temur Kutsia and Cleo Pau},
title = {{Solving Proximity Constraints}},
language = {english},
number = {19-06},
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 = {Temur Kutsia and Cleo Pau},
title = {{Solving Proximity Constraints}},
language = {english},
number = {19-06},
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}
}
[Pau]
Matching and Generalization Modulo Proximity and Tolerance
Temur Kutsia, Cleo Pau
Technical report no. 19-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]@techreport{RISC5953,
author = {Temur Kutsia and Cleo Pau},
title = {{Matching and Generalization Modulo Proximity and Tolerance}},
language = {english},
number = {19-07},
year = {2019},
length = {5},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
author = {Temur Kutsia and Cleo Pau},
title = {{Matching and Generalization Modulo Proximity and Tolerance}},
language = {english},
number = {19-07},
year = {2019},
length = {5},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Schreiner]
McCarthy-Kleene fuzzy automata and MSO logics
Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner
Information and Computation, pp. -. 2019. Elsevier, ISSN 0890-5401. In Press. [url]@article{RISC6011,
author = {Manfred Droste and Temur Kutsia and George Rahonis and Wolfgang Schreiner},
title = {{McCarthy-Kleene fuzzy automata and MSO logics}},
language = {english},
abstract = {We introduce McCarthy-Kleene fuzzy automata (MK-fuzzy automata) over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a Büchi type theorem.},
journal = {Information and Computation},
pages = {--},
publisher = {Elsevier},
isbn_issn = {ISSN 0890-5401},
year = {2019},
note = {In Press},
refereed = {yes},
keywords = {Bimonoids, McCarthy-Kleene logic, MK-fuzzy automata, MK-fuzzy MSO logic},
sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program 846003 “LogicGuard II”},
length = {23},
url = {https://doi.org/10.1016/j.ic.2019.104499}
}
author = {Manfred Droste and Temur Kutsia and George Rahonis and Wolfgang Schreiner},
title = {{McCarthy-Kleene fuzzy automata and MSO logics}},
language = {english},
abstract = {We introduce McCarthy-Kleene fuzzy automata (MK-fuzzy automata) over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a Büchi type theorem.},
journal = {Information and Computation},
pages = {--},
publisher = {Elsevier},
isbn_issn = {ISSN 0890-5401},
year = {2019},
note = {In Press},
refereed = {yes},
keywords = {Bimonoids, McCarthy-Kleene logic, MK-fuzzy automata, MK-fuzzy MSO logic},
sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program 846003 “LogicGuard II”},
length = {23},
url = {https://doi.org/10.1016/j.ic.2019.104499}
}
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}
}
[Baumgartner]
Term-Graph Anti-Unification
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret
In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Helene Kirchner (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 108, pp. 9:1-9:17. 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, ISBN 978-3-95977-077-4 ISSN 1868-8969. [url]@inproceedings{RISC5764,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {108},
pages = {9:1--9:17},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},
year = {2018},
editor = {Helene Kirchner},
refereed = {yes},
length = {17},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9179}
}
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {108},
pages = {9:1--9:17},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},
year = {2018},
editor = {Helene Kirchner},
refereed = {yes},
length = {17},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9179}
}
[Cerna]
Idempotent Anti-unification
David M. Cerna, Temur Kutsia
RISC. Technical report, Feb. 2018. to appear in TOCL. [pdf]@techreport{RISC5530,
author = {David M. Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification }},
language = {english},
abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},
year = {2018},
month = {Feb.},
note = {to appear in TOCL},
institution = {RISC},
length = {32}
}
author = {David M. Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification }},
language = {english},
abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},
year = {2018},
month = {Feb.},
note = {to appear in TOCL},
institution = {RISC},
length = {32}
}
[Cerna]
Primitive Recursive Proof Systems for Arithmetic
David M. Cerna
RISC. Technical report, January 2018. In revision. [pdf] [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]
Higher-Order Equational Pattern Anti-Unification
David M. Cerna, Temur Kutsia
In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Helene Kirchner (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 108, pp. 12:1-12:17. 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, ISBN 978-3-95977-077-4 ISSN 1868-8969. [url]@inproceedings{RISC5765,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Equational Pattern Anti-Unification}},
booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {108},
pages = {12:1--12:17},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},
year = {2018},
editor = {Helene Kirchner},
refereed = {yes},
length = {17},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9182}
}
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Equational Pattern Anti-Unification}},
booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {108},
pages = {12:1--12:17},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},
year = {2018},
editor = {Helene Kirchner},
refereed = {yes},
length = {17},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9182}
}
[Dramnesc]
Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat
Journal of Symbolic Computation 90, pp. 3-41. 2018. Elsevier, 07477171. [url]@article{RISC5715,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {90},
pages = {3--41},
publisher = {Elsevier},
isbn_issn = {07477171},
year = {2018},
refereed = {yes},
keywords = {algorithm synthesis ; automated reasoning ; natural--style proving},
length = {39},
url = {https://doi.org/10.1016/j.jsc.2018.04.002}
}
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {90},
pages = {3--41},
publisher = {Elsevier},
isbn_issn = {07477171},
year = {2018},
refereed = {yes},
keywords = {algorithm synthesis ; automated reasoning ; natural--style proving},
length = {39},
url = {https://doi.org/10.1016/j.jsc.2018.04.002}
}
[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}
}
[Jebelean]
Experiments with Automatic Proofs in Elementary Analysis
T. Jebelean
Technical report no. 18-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2018. Work in progress. [pdf] [zip] [pdf]@techreport{RISC5692,
author = {T. Jebelean},
title = {{Experiments with Automatic Proofs in Elementary Analysis}},
language = {english},
abstract = {Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non--clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms.We demonstrate on some concrete examples several heuristic techniques for the automation of natural--style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra.Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions.These techniques are being implemented in the {\em Theorema} system and are able to construct automatically natural--style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.},
number = {18-06},
year = {2018},
month = {April},
keywords = {Satisfiability Checking, Natural-style Proofs, Symbolic Computation},
sponsor = {European project ``Satisfiability Checking and Symbolic Computation'' (H2020-FETOPN-2015-CSA 712689)},
length = {33},
type = {Work in progress},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
author = {T. Jebelean},
title = {{Experiments with Automatic Proofs in Elementary Analysis}},
language = {english},
abstract = {Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non--clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms.We demonstrate on some concrete examples several heuristic techniques for the automation of natural--style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra.Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions.These techniques are being implemented in the {\em Theorema} system and are able to construct automatically natural--style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.},
number = {18-06},
year = {2018},
month = {April},
keywords = {Satisfiability Checking, Natural-style Proofs, Symbolic Computation},
sponsor = {European project ``Satisfiability Checking and Symbolic Computation'' (H2020-FETOPN-2015-CSA 712689)},
length = {33},
type = {Work in progress},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[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}
}
