Institute e-Austria Timisoara: Mathematical Theory Exploration for Industrial Applications [iEAT]
Project Lead
Project Duration
01/03/2008 - 28/02/2011Software
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
MoreSoftware WebsitePublications
2017
[Buchberger]
Gröbner Bases Computation by Triangularizing Macaulay Matrices
Bruno Buchberger
Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases) 75, pp. 1-9. 2017. Mathematical Society of Japan, 0.@article{RISC5586,
author = {Bruno Buchberger},
title = {{Gröbner Bases Computation by Triangularizing Macaulay Matrices}},
language = {english},
journal = {Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases)},
volume = {75},
pages = {1--9},
publisher = {Mathematical Society of Japan},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {9}
}
author = {Bruno Buchberger},
title = {{Gröbner Bases Computation by Triangularizing Macaulay Matrices}},
language = {english},
journal = {Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases)},
volume = {75},
pages = {1--9},
publisher = {Mathematical Society of Japan},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {9}
}
[Buchberger]
Satisfiability Checking and Symbolic Computation
Abraham Erika , Abbott John , Becker Bernd , Bigatti Anna Maria , Brain Martin , Buchberger Bruno , Cimatti Alessandro , Davenport James , England Matthew , Fontaine Pascal , Forrest Stephen , Griggio Alberto , Kröning Daniel , Seiler Werner M. , Sturm
ACM Communications in Computer Algebra 50(4), pp. 145-147. 2017. 0.@article{RISC5587,
author = { Abraham Erika and Abbott John and Becker Bernd and Bigatti Anna Maria and Brain Martin and Buchberger Bruno and Cimatti Alessandro and Davenport James and England Matthew and Fontaine Pascal and Forrest Stephen and Griggio Alberto and Kröning Daniel and Seiler Werner M. and Sturm },
title = {{Satisfiability Checking and Symbolic Computation}},
language = {english},
journal = {ACM Communications in Computer Algebra},
volume = {50},
number = {4},
pages = {145--147},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {3}
}
author = { Abraham Erika and Abbott John and Becker Bernd and Bigatti Anna Maria and Brain Martin and Buchberger Bruno and Cimatti Alessandro and Davenport James and England Matthew and Fontaine Pascal and Forrest Stephen and Griggio Alberto and Kröning Daniel and Seiler Werner M. and Sturm },
title = {{Satisfiability Checking and Symbolic Computation}},
language = {english},
journal = {ACM Communications in Computer Algebra},
volume = {50},
number = {4},
pages = {145--147},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {3}
}
2016
[Maletzky]
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]@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}
}
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}
}
2015
[Dramnesc]
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, ..@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}
}
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}
}
[Dramnesc]
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]@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)}
}
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)}
}
2011
[Buchberger]
Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Groebner Bases
Markus Rosenkranz, Georg Regensburger, Loredana Tec, Bruno Buchberger
In: Numerical and Symbolic Scientific Computing: Progress and Prospects, Ulrich Langer and Peter Paule (ed.), pp. 273-331. 2011. Springer, Wien, ISBN 978-3-7091-0793-5. Also available as RICAM Report 2010-05, September 2010. [pdf]@incollection{RISC4330,
author = {Markus Rosenkranz and Georg Regensburger and Loredana Tec and Bruno Buchberger},
title = {{Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Groebner Bases}},
booktitle = {{Numerical and Symbolic Scientific Computing: Progress and Prospects}},
language = {english},
pages = {273--331},
publisher = {Springer, Wien},
isbn_issn = {ISBN 978-3-7091-0793-5},
year = {2011},
annote = {2011-00-00-A},
note = {Also available as RICAM Report 2010-05, September 2010},
editor = {Ulrich Langer and Peter Paule},
refereed = {yes},
length = {54}
}
author = {Markus Rosenkranz and Georg Regensburger and Loredana Tec and Bruno Buchberger},
title = {{Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Groebner Bases}},
booktitle = {{Numerical and Symbolic Scientific Computing: Progress and Prospects}},
language = {english},
pages = {273--331},
publisher = {Springer, Wien},
isbn_issn = {ISBN 978-3-7091-0793-5},
year = {2011},
annote = {2011-00-00-A},
note = {Also available as RICAM Report 2010-05, September 2010},
editor = {Ulrich Langer and Peter Paule},
refereed = {yes},
length = {54}
}
[Buchberger]
Buchberger's Algorithm
Bruno Buchberger, Manuel Kauers
Scholarpedia 6(10), pp. 7764-7764. October 2011. 1941-6016. [url]@article{RISC4394,
author = {Bruno Buchberger and Manuel Kauers},
title = {{Buchberger's Algorithm}},
language = {english},
journal = {Scholarpedia},
volume = {6},
number = {10},
pages = {7764--7764},
isbn_issn = {1941-6016},
year = {2011},
month = {October},
annote = {2011-10-00-A},
refereed = {yes},
length = {1},
url = {http://www.scholarpedia.org/article/Buchberger%27s_algorithm}
}
author = {Bruno Buchberger and Manuel Kauers},
title = {{Buchberger's Algorithm}},
language = {english},
journal = {Scholarpedia},
volume = {6},
number = {10},
pages = {7764--7764},
isbn_issn = {1941-6016},
year = {2011},
month = {October},
annote = {2011-10-00-A},
refereed = {yes},
length = {1},
url = {http://www.scholarpedia.org/article/Buchberger%27s_algorithm}
}
[Kusper]
SAT Solving Experiments in Multi-Domain Logic
Tudor Jebelean, Gabor Kusper
In: ICAI 2001, Emod Kovacs (ed.)I, pp. 95-105. 2011. Eger, Hungary, 0.@inproceedings{RISC4355,
author = {Tudor Jebelean and Gabor Kusper},
title = {{SAT Solving Experiments in Multi-Domain Logic}},
booktitle = {{ICAI 2001}},
language = {english},
volume = {I},
pages = {95--105},
address = {Eger, Hungary},
isbn_issn = {0},
year = {2011},
editor = {Emod Kovacs},
refereed = {yes},
length = {11}
}
author = {Tudor Jebelean and Gabor Kusper},
title = {{SAT Solving Experiments in Multi-Domain Logic}},
booktitle = {{ICAI 2001}},
language = {english},
volume = {I},
pages = {95--105},
address = {Eger, Hungary},
isbn_issn = {0},
year = {2011},
editor = {Emod Kovacs},
refereed = {yes},
length = {11}
}
[Popov]
Sound and Complete Verification Condition Generator for Functional Recursive Programs.
N. Popov, T. Jebelean
In: Numerical and Symbolic Scientific Computing: Progress and Prospects, U. Langer and P. Paule (ed.), pp. 219-256. 2011. Springer, Wien, ISBN 978-3-7091-0793-5.@incollection{RISC4342,
author = {N. Popov and T. Jebelean},
title = {{Sound and Complete Verification Condition Generator for Functional Recursive Programs.}},
booktitle = {{Numerical and Symbolic Scientific Computing: Progress and Prospects}},
language = {english},
pages = {219--256},
publisher = {Springer},
address = {Wien},
isbn_issn = {ISBN 978-3-7091-0793-5},
year = {2011},
editor = {U. Langer and P. Paule},
refereed = {yes},
length = {38}
}
author = {N. Popov and T. Jebelean},
title = {{Sound and Complete Verification Condition Generator for Functional Recursive Programs.}},
booktitle = {{Numerical and Symbolic Scientific Computing: Progress and Prospects}},
language = {english},
pages = {219--256},
publisher = {Springer},
address = {Wien},
isbn_issn = {ISBN 978-3-7091-0793-5},
year = {2011},
editor = {U. Langer and P. Paule},
refereed = {yes},
length = {38}
}
2010
[Buchberger]
From Program Verification to Automated Debugging
N. Popov, T. Jebelean, B. Buchberger
In: Workshop on Symbolic Computation in Software Science, T. Jebelean and M. Mosbah and N. Popov (ed.), Proceedings of SCSS 2010, pp. 55-65. July 2010. RISC-Linz Report Series, Johannes Kepler University of Linz, Austria, ..@inproceedings{RISC4192,
author = {N. Popov and T. Jebelean and B. Buchberger},
title = {{From Program Verification to Automated Debugging}},
booktitle = {{Workshop on Symbolic Computation in Software Science}},
language = {english},
pages = {55--65},
publisher = {RISC-Linz Report Series},
isbn_issn = {.},
year = {2010},
month = {July},
annote = {2010-07-00-A},
editor = {T. Jebelean and M. Mosbah and N. Popov},
refereed = {yes},
institution = {Johannes Kepler University of Linz, Austria},
length = {11},
conferencename = {SCSS 2010}
}
author = {N. Popov and T. Jebelean and B. Buchberger},
title = {{From Program Verification to Automated Debugging}},
booktitle = {{Workshop on Symbolic Computation in Software Science}},
language = {english},
pages = {55--65},
publisher = {RISC-Linz Report Series},
isbn_issn = {.},
year = {2010},
month = {July},
annote = {2010-07-00-A},
editor = {T. Jebelean and M. Mosbah and N. Popov},
refereed = {yes},
institution = {Johannes Kepler University of Linz, Austria},
length = {11},
conferencename = {SCSS 2010}
}
[Popov]
Projects of Evidence Algorithm and Theorema
A. Anisimov, T. Jebelean, A. Lyaletski, N. Popov
In: Theoretical and Applied Aspects of Program Systems Development, A. Anisimov, V. Redko (ed.), pp. 54-58. October 2010. Kiev, Ukraine, ..@inproceedings{RISC4195,
author = {A. Anisimov and T. Jebelean and A. Lyaletski and N. Popov},
title = {{Projects of Evidence Algorithm and Theorema}},
booktitle = {{Theoretical and Applied Aspects of Program Systems Development}},
language = {russian},
pages = {54--58},
address = {Kiev, Ukraine},
isbn_issn = {.},
year = {2010},
month = {October},
editor = {A. Anisimov and V. Redko},
refereed = {yes},
length = {5}
}
author = {A. Anisimov and T. Jebelean and A. Lyaletski and N. Popov},
title = {{Projects of Evidence Algorithm and Theorema}},
booktitle = {{Theoretical and Applied Aspects of Program Systems Development}},
language = {russian},
pages = {54--58},
address = {Kiev, Ukraine},
isbn_issn = {.},
year = {2010},
month = {October},
editor = {A. Anisimov and V. Redko},
refereed = {yes},
length = {5}
}
[Popov]
Proceedings of SCSS 2010 Symbolic Computation in Software Science
T. Jebelean, M. Mosbah, N. Popov (eds.)
Technical report no. 10-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2010. [pdf]@techreport{RISC4191,
author = {T. Jebelean and M. Mosbah and N. Popov (eds.)},
title = {{Proceedings of SCSS 2010 Symbolic Computation in Software Science}},
language = {english},
number = {10-10},
year = {2010},
month = {August},
length = {160},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
author = {T. Jebelean and M. Mosbah and N. Popov (eds.)},
title = {{Proceedings of SCSS 2010 Symbolic Computation in Software Science}},
language = {english},
number = {10-10},
year = {2010},
month = {August},
length = {160},
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)}
}
[Popov]
Proving Partial Correctness and Termination of Mutually Recursive Programs
N. Popov, T. Jebelean
In: SYNASC 2010, T. Ida, V. Negru, T. Jebelean, D. Petcu, S. Watt, and, D. Zaharie (ed.), Proceedings of Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 153-158. September 2010. IEEE , ISBN 978-0-7695-4324-6. [pdf]@inproceedings{RISC4287,
author = {N. Popov and T. Jebelean},
title = {{Proving Partial Correctness and Termination of Mutually Recursive Programs}},
booktitle = {{SYNASC 2010}},
language = {english},
pages = {153--158},
publisher = {IEEE },
isbn_issn = {ISBN 978-0-7695-4324-6},
year = {2010},
month = {September},
editor = {T. Ida and V. Negru and T. Jebelean and D. Petcu and S. Watt and and and D. Zaharie},
refereed = {yes},
length = {5},
conferencename = {Symposium on Symbolic and Numeric Algorithms for Scientific Computing}
}
author = {N. Popov and T. Jebelean},
title = {{Proving Partial Correctness and Termination of Mutually Recursive Programs}},
booktitle = {{SYNASC 2010}},
language = {english},
pages = {153--158},
publisher = {IEEE },
isbn_issn = {ISBN 978-0-7695-4324-6},
year = {2010},
month = {September},
editor = {T. Ida and V. Negru and T. Jebelean and D. Petcu and S. Watt and and and D. Zaharie},
refereed = {yes},
length = {5},
conferencename = {Symposium on Symbolic and Numeric Algorithms for Scientific Computing}
}
1994
[Jebelean]
Systolic Multiprecision Arithmetics
Tudor Jebelean
RISC, Johannes Kepler University Linz. PhD Thesis. 1994.@phdthesis{RISC4134,
author = {Tudor Jebelean},
title = {{Systolic Multiprecision Arithmetics}},
language = {english},
year = {1994},
translation = {0},
school = {RISC, Johannes Kepler University Linz},
length = {0}
}
author = {Tudor Jebelean},
title = {{Systolic Multiprecision Arithmetics}},
language = {english},
year = {1994},
translation = {0},
school = {RISC, Johannes Kepler University Linz},
length = {0}
}
