A.Univ.-Prof. Dr. Tudor Jebelean

Research Area

Automated Reasoning, Systolic Computations, Multiprecision Arithmetic

WWW

Personal home page

Ongoing Projects

Theorema Project

Project Lead: Bruno Buchberger

Project Duration: 01/01/1994 -

The present prototype version of the Theorema software system is implemented in Mathematica . The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. ...

Authors: Alexander Maletzky, Bruno Buchberger, Markus Rosenkranz, Nikolaj Popov, Teimuraz Kutsia, Tudor Jebelean, Wolfgang Windsteiger

More Software Website

Publications

2021

[Jebelean]

A Heuristic Prover for Elementary Analysis in Theorema

Tudor Jebelean

Technical report no. 21-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]

[bib]

@techreport{RISC6293,
author = {Tudor Jebelean},
title = {{A Heuristic Prover for Elementary Analysis in Theorema}},
language = {english},
abstract = {We present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions, and continuity of the composition of functions.},
number = {21-07},
year = {2021},
month = {April},
keywords = {Theorema, S-decomposition, automated theorem proving},
length = {29},
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)}
}

[Jebelean]

A Heuristic Prover for Elementary Analysis in Theorema

T. Jebelean

In: Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania, F. Kamaredine, C. Sacerdoti Coen (ed.), Proceedings of Intelligent Computer Mathematics, 14th International Conference, CICM 2021, LNAI 12833, pp. 130-134. July 2021. Springer, 978-3-030-81096-2. [pdf]

[bib]

@inproceedings{RISC6477,
author = {T. Jebelean},
title = {{A Heuristic Prover for Elementary Analysis in Theorema}},
booktitle = {{Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania}},
language = {english},
abstract = { We present a plug-in to the Theorema system, which generates proofs similar to those produced by humans for theorems in elementary analysis and is based on heuristic techniques combining methods from automated reasoning and computer algebra. The prover is able to construct automatically natural-style proofs for various examples related to convergence of sequences as well as to limits, continuity, and uniform continuity of functions. Additionally to general inference rules for predicate logic, the techniques used are: the S-decomposition method for formulae with alternating quantifiers, use of Quantifier Elimination by Cylindrical Algebraic Decomposition, analysis of terms behavior in zero, bounding the epsilon-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admissibility of solutions to the metavariables. The problem of proving such theorems directly without using refutation and clausification is logically equivalent to the problem of satisfiability modulo the theory of real numbers, thus these techniques are relevant for SMT solving also.},
series = {LNAI},
volume = {12833},
pages = {130--134},
publisher = {Springer},
isbn_issn = {978-3-030-81096-2},
year = {2021},
month = {July},
editor = {F. Kamaredine and C. Sacerdoti Coen},
refereed = {yes},
keywords = {Satisfiability Checking, Natural-style Proofs, Computer Algebra, Symbolic Computation, Satisfiability Modulo Theories},
length = {5},
conferencename = {Intelligent Computer Mathematics, 14th International Conference, CICM 2021}
}

[Jebelean]

AlCons: Deductive Synthesis of Sorting Algorithms in Theorema

I. Dramnesc, T. Jebelean

In: Theoretical Aspects of Computing - ICTAC 2021, A. Cerone, P. Csaba Ölveczky (ed.), Proceedings of 18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan, LNCS 12819, pp. 314-333. September 2021. Springer, 978-3-030-85315-0. [pdf]

[bib]

@inproceedings{RISC6478,
author = {I. Dramnesc and T. Jebelean},
title = {{AlCons: Deductive Synthesis of Sorting Algorithms in Theorema}},
booktitle = {{Theoretical Aspects of Computing - ICTAC 2021}},
language = {english},
abstract = {We describe the principles and the implementation of AlCons (em Algorithm Constructor), a system for the automatic proof--based synthesis of sorting algorithms on lists and on binary trees, in the frame of the Theorema system. The core of the system is a dedicated prover based on specific inference rules and strategies for constructive proofs over the domains of lists and of binary trees, aimed at the automatic synthesis of sorting algorithms and their auxiliary functions from logical specifications. The specific distinctive feature of our approach is the use of multisets for expressing the fact that two lists (trees) have the same elements. This allows a more natural expression of the properties related to sorting, compared to the classical approach using the permutation relation (a list is a permutation of another). Moreover, the use of multisets leads to special inference rules and strategies which make the proofs more efficient, as for instance: expand/compress multiset terms and solve meta-variables using multiset equalities. Additionally we use a Noetherian induction strategy based on the relation induced by the strict inclusion of multisets, which facilitates the synthesis of arbitrary recursion structures, without having to indicate the recursion schemes in advance. The necessary auxiliary algorithms (like, e.g., for insertion and merging) are generated by the same principles from the synthesis conjectures that are automatically produced during the main proof, using a ``cascading" method, which in fact contributes to the automation of theory exploration. The prover is implemented in the frame of the Theorema system and works in natural style, while the generated algorithms can be immediately tested in the same system.},
series = {LNCS},
volume = {12819},
pages = {314--333},
publisher = {Springer},
isbn_issn = {978-3-030-85315-0},
year = {2021},
month = {September },
editor = {A. Cerone and P. Csaba Ölveczky},
refereed = {yes},
length = {20},
conferencename = {18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan}
}

2020

[Jebelean]

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]

[bib]

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

[Jebelean]

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]

[bib]

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

2018

[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, Austria. ISSN 2791-4267 (online). April 2018. Work in progress. [zip] [pdf] [pdf]

[bib]

@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

[Jebelean]

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. [doi]

[bib]

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

2017

[Jebelean]

A Set-Based Approach to Qualitative and Quantitative Estimation of Competencies

Tudor Jebelean, Nikolaj Popov

Technical report no. 17-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). September 2017. [pdf]

[bib]

@techreport{RISC5486,
author = {Tudor Jebelean and Nikolaj Popov},
title = {{A Set-Based Approach to Qualitative and Quantitative Estimation of Competencies}},
language = {english},
abstract = {We present a novel strategy for making non-trivial matches ofposition openings versus job applications. The strategy forms a logicallybased framework for the development of a real system which ensures a correctand an efficient matching.In our framework, we translate the notions of knowledge and skills intoabstract mathematical sets. The sets are classified and ordered, as the skillsare in the real life. The operations of finding similarities between skills arethen made as set intersections based on the mathematical apparatus for set operations.Moreover, this theoretical model gives not only the possibility to decide if twoobjects are similar or not, but also it defines a distance between them.Based on that distance, one may compute the effort needed for a job applicant to fulfillprecise job descriptions.},
number = {17-05},
year = {2017},
month = {September},
length = {20},
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)}
}

[Jebelean]

Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks

E. Abraham, T. Jebelean

In: ICAI 2017: 10th International Conference on Applied Informatics, G. Kusper (ed.), Proceedings of ICAI 2017: 10th International Conference on Applied Informatics, pp. 0-0. 2017. ISBN 0. In print. [url] [pdf]

[bib]

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

2016

[Jebelean]

Proof-based Synthesis of Sorting Algorithms for Trees

Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat

In: Proceedings of LATA 2016, the 10th International Conference on Language and Automata Theory and Applications, Adrian-Horia Dediu, Jan Janousek, Carlos Martin-Vide, Bianca Truthe (ed.), Proceedings of LATA 2016, LNCS 9618, pp. 562-575. 2016. Springer, ISBN 978-3-319-29999-0.

[bib]

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

[Jebelean]

Theorema 2.0: Computer-Assisted Natural-Style Mathematics

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

JFR 9(1), pp. 149-185. 2016. ISSN 1972-5787. [doi]

[bib]

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

[Jebelean]

A case study on algorithm discovery from proofs: The insert function on binary trees

Isabela Dramnesc and Tudor Jebelean, Sorin Stratulat

In: 11th IEEE International Symposium on Applied Computational Intelligence and Informatics, SACI 2016, Timisoara, Romania, May 12-14, 2016, IEEE (ed.), pp. 231-236. 2016. 978-1-5090-2380-6. [doi]

[bib]

@inproceedings{RISC5714,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{A case study on algorithm discovery from proofs: The insert function on binary trees}},
booktitle = {{11th IEEE International Symposium on Applied Computational Intelligence and Informatics, SACI 2016, Timisoara, Romania, May 12-14, 2016}},
language = {english},
pages = {231--236},
isbn_issn = {978-1-5090-2380-6},
year = {2016},
editor = {IEEE},
refereed = {yes},
length = {6},
url = {https://doi.org/10.1109/SACI.2016.7507376}
}

2015

[Jebelean]

Combinatorial Techniques for Proof-based Synthesis of Sorting Algorithms

Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat

In: SYNASC 2015: Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Laura Kovacs (ed.), pp. 137-144. 2015. IEEE Computer Society, ISBN 978-0-7695-5742-2.

[bib]

@inproceedings{RISC5423,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Combinatorial Techniques for Proof-based Synthesis of Sorting Algorithms}},
booktitle = {{SYNASC 2015: Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing}},
language = {english},
pages = {137--144},
publisher = {IEEE Computer Society},
isbn_issn = {ISBN 978-0-7695-5742-2},
year = {2015},
editor = {Laura Kovacs},
refereed = {yes},
length = {8}
}

[Jebelean]

Synthesis of list algorithms by mechanical proving

Isabela Dramnesc, Tudor Jebelean

Journal of Symbolic Computation 69, pp. 61-92. 2015. ISSN 0747-7171.

[bib]

@article{RISC5083,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Synthesis of list algorithms by mechanical proving}},
language = {english},
abstract = {We address the automation of the processes of algorithm synthesis and systematic exploration of the theory of lists. Our focus is on methods, techniques, inference rules and strategies for computer based synthesis of list algorithms based on proving. Starting from the specification of the problem (input and output conditions), a synthesis statement is built: “for any list satisfying the input condition, there exists a list satisfying the output condition”. The main difficulty is to find a constructive proof of this statement, from which the corresponding algorithm is easily extracted as a set of conditional equalities.In more detail, we aim at computer automation of the proof of the existence of the sorted version of the input list. By using different proof methods we automatically synthesize five sorting algorithms: Selection-Sort, Insertion-Sort, Quick-Sort, Merge-Sort, and a novel algorithm, which we call Unbalanced-Merge-Sort, as well as the auxiliary functions used in the sorting algorithms. The theory we use is first order, and mostly contains formulae which are equivalent to Horn clauses. Therefore, except for induction, SLD resolution style inferences are in principle sufficient for performing the proofs. However, for most of the proofs this leads to a very large search space. Therefore we introduce several novel inference rules and specific strategies, which are based on the properties of lists, and which we developed in the course of this case study on sorting.Moreover, during the process of algorithm synthesis we explore the theory of lists by introducing (automatically prove, and then use) the necessary properties.When the knowledge base does not contain the auxiliary functions needed for the respective version of the algorithm, then the proof fails and from this failure a new proof goal is created, which is the synthesis statement for the missing auxiliary functions (“cascading”).},
journal = {Journal of Symbolic Computation},
volume = {69},
pages = {61--92},
isbn_issn = {ISSN 0747-7171},
year = {2015},
refereed = {yes},
sponsor = {Partially supported by the European Commission grant No. FP7-REGPOT-CT-2011-284595 (HOST).},
length = {32}
}

[Jebelean]

Synthesis of Some Algorithms for Trees: Experiments in Theorema

Isabela Dramnesc, Tudor Jebelean and Sorin Stratulat

Technical report no. 15-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2015. [pdf]

[bib]

@techreport{RISC5147,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Synthesis of Some Algorithms for Trees: Experiments in Theorema}},
language = {english},
number = {15-04},
year = {2015},
length = {57},
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)}
}

[Jebelean]

A Case Study in Proof Based Synthesis of Algorithms on Monotone Lists

Isabela Dramnesc, Tudor Jebelean

In: The 10th International Symposium on Applied Computational Intelligence and Informatics, . (ed.), Proceedings of SACI 2015, pp. 483-488. 2015. IEEE Xplore, _.

[bib]

@inproceedings{RISC5148,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{A Case Study in Proof Based Synthesis of Algorithms on Monotone Lists}},
booktitle = {{The 10th International Symposium on Applied Computational Intelligence and Informatics}},
language = {english},
pages = {483--488},
publisher = {IEEE Xplore},
isbn_issn = {_},
year = {2015},
editor = {.},
refereed = {yes},
length = {6},
conferencename = {SACI 2015}
}

[Jebelean]

Theory Exploration of Binary Trees

Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat

In: The IEEE 13th Jubilee International Symposium on Intelligent Systems and Informatics, . (ed.), Proceedings of SISY 2015, pp. 139-144. 2015. IEEE Xplore, ..

[bib]

@inproceedings{RISC5165,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Theory Exploration of Binary Trees}},
booktitle = {{The IEEE 13th Jubilee International Symposium on Intelligent Systems and Informatics}},
language = {english},
pages = {139--144},
publisher = {IEEE Xplore},
isbn_issn = {.},
year = {2015},
editor = {.},
refereed = {yes},
length = {6},
conferencename = {SISY 2015}
}

2014

[Jebelean]

Theory Exploration of Sets Represented as Monotone Lists

Isabela Dramnesc, Tudor Jebelean

In: Proceedings of SISY 2014 IEEE 12th International Symposium on Intelligent Systems and Informatics, IEEE Xplore (ed.), pp. 163-168. 2014. ..

[bib]

@inproceedings{RISC5128,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Theory Exploration of Sets Represented as Monotone Lists}},
booktitle = {{Proceedings of SISY 2014 IEEE 12th International Symposium on Intelligent Systems and Informatics}},
language = {english},
pages = {163--168},
isbn_issn = { .},
year = {2014},
editor = {IEEE Xplore},
refereed = {yes},
length = {6}
}

2012

[Jebelean]

Formalization of Workflows Using Fork-Join Automata

Tudor Jebelean, Anna Medve

Technical report no. 12-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). December 2012. [pdf]

[bib]

@techreport{RISC4409,
author = {Tudor Jebelean and Anna Medve},
title = {{Formalization of Workflows Using Fork-Join Automata}},
language = {english},
abstract = {We survey the current practice of using workflows for business process modeling and we present a simple formalism for reasoning about the structural correctness of fork-join workflow diagrams containing {\em and} and {\em or} nodes.},
number = {12-21},
year = {2012},
month = {December},
length = {7},
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)}
}

[Jebelean]

Semi-automatic Synthesis of Some Sorting Programs in Theorema

Isabela Dramnesc, Tudor Jebelean

Research Institute for Symbolic Computation (RISC), University of Linz. Technical report no. 12-01, Schloss Hagenberg, 4232 Hagenberg, Austria, January 2012. RISC Report Series. [pdf]

[bib]

@techreport{RISC4410,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Semi-automatic Synthesis of Some Sorting Programs in Theorema}},
language = {english},
number = {12-01},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria},
year = {2012},
month = {January},
institution = {Research Institute for Symbolic Computation (RISC), University of Linz},
length = {0},
type = {RISC Report Series}
}