# e-Austria Timisoara: Pilot Phase I

### Project Description

B. Buchberger, T. Jebelean.

Budget: 100.000,– Eur.

Projektbeginn bzw. Projectende 2003:

### Project Lead

### Project Duration

01/03/2002 - 30/06/2003## Publications

### 2017

### 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.@

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}

}

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

}

### 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.@

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}

}

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

}

### 2015

### 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, ..@

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}

}

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

}

### 2011

### 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]@

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}

}

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

}

### Buchberger's Algorithm

#### Bruno Buchberger, Manuel Kauers

Scholarpedia 6(10), pp. 7764-7764. October 2011. 1941-6016. [url]@

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}

}

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

}

### 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.@

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}

}

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

}

### 2010

### An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra

#### Loredana Tec, Georg Regensburger, Markus Rosenkranz and Bruno Buchberger

In: Mathematical Software - ICMS 2010, Third International Congress on Mathematical Software, Kobe, Japan, September 13-17, Komei Fukuda and Joris van der Hoeven and Michael Joswig and Nobuki Takayama (ed.), Proceedings of ICMS, Lecture Notes in Computer Science 6327, pp. 245-248. 2010. Springer, 978-3-642-15581-9. [pdf]@

author = {Loredana Tec and Georg Regensburger and Markus Rosenkranz and Bruno Buchberger},

title = {{An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra}},

booktitle = {{Mathematical Software - ICMS 2010, Third International Congress on Mathematical Software, Kobe, Japan, September 13-17}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {6327},

pages = {245--248},

publisher = {Springer},

isbn_issn = {978-3-642-15581-9},

year = {2010},

annote = {2010-09-00-A},

editor = {Komei Fukuda and Joris van der Hoeven and Michael Joswig and Nobuki Takayama},

refereed = {yes},

length = {4},

conferencename = {ICMS}

}

**inproceedings**{RISC4044,author = {Loredana Tec and Georg Regensburger and Markus Rosenkranz and Bruno Buchberger},

title = {{An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra}},

booktitle = {{Mathematical Software - ICMS 2010, Third International Congress on Mathematical Software, Kobe, Japan, September 13-17}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {6327},

pages = {245--248},

publisher = {Springer},

isbn_issn = {978-3-642-15581-9},

year = {2010},

annote = {2010-09-00-A},

editor = {Komei Fukuda and Joris van der Hoeven and Michael Joswig and Nobuki Takayama},

refereed = {yes},

length = {4},

conferencename = {ICMS}

}

### Groebner Bases

#### Bruno Buchberger, Manuel Kauers

Scholarpedia 5(10), pp. 7763-7763. October 2010. ISSN 1941-6016. [url]@

author = {Bruno Buchberger and Manuel Kauers},

title = {{Groebner Bases}},

language = {english},

journal = {Scholarpedia},

volume = {5},

number = {10},

pages = {7763--7763},

isbn_issn = {ISSN 1941-6016},

year = {2010},

month = {October},

annote = {2010-10-00-A},

refereed = {yes},

length = {16},

url = {http://www.scholarpedia.org/article/Groebner_basis}

}

**article**{RISC4161,author = {Bruno Buchberger and Manuel Kauers},

title = {{Groebner Bases}},

language = {english},

journal = {Scholarpedia},

volume = {5},

number = {10},

pages = {7763--7763},

isbn_issn = {ISSN 1941-6016},

year = {2010},

month = {October},

annote = {2010-10-00-A},

refereed = {yes},

length = {16},

url = {http://www.scholarpedia.org/article/Groebner_basis}

}

### 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, ..@

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}

}

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

}

### 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, ..@

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}

}

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

}

### 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]@

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}

}

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

}

### 2009

### Automated Reasoning

#### Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger

In: Hagenberg Research, B. Buchberger, M. Affenzeller, A. Ferscha, M. Haller, T. Jebelean, E.P. Klement, P. Paule, G. Pomberger, W. Schreiner, R. Stubenrauch, R. Wagner, G. Weiss, W. Windsteiger (ed.), pp. 63-101. 2009. Springer Dordrecht Heidelberg London New York, ISBN 978-3-642-02126-8. [url]@

author = {Tudor Jebelean and Bruno Buchberger and Temur Kutsia and Nikolaj Popov and Wolfgang Schreiner and Wolfgang Windsteiger},

title = {{Automated Reasoning}},

booktitle = {{Hagenberg Research}},

language = {english},

pages = {63--101},

publisher = {Springer Dordrecht Heidelberg London New York},

isbn_issn = {ISBN 978-3-642-02126-8},

year = {2009},

annote = {2009-00-00-B},

editor = {B. Buchberger and M. Affenzeller and A. Ferscha and M. Haller and T. Jebelean and E.P. Klement and P. Paule and G. Pomberger and W. Schreiner and R. Stubenrauch and R. Wagner and G. Weiss and W. Windsteiger},

refereed = {no},

length = {39},

url = {http://www.springer.com/computer/programming/book/978-3-642-02126-8}

}

**incollection**{RISC3844,author = {Tudor Jebelean and Bruno Buchberger and Temur Kutsia and Nikolaj Popov and Wolfgang Schreiner and Wolfgang Windsteiger},

title = {{Automated Reasoning}},

booktitle = {{Hagenberg Research}},

language = {english},

pages = {63--101},

publisher = {Springer Dordrecht Heidelberg London New York},

isbn_issn = {ISBN 978-3-642-02126-8},

year = {2009},

annote = {2009-00-00-B},

editor = {B. Buchberger and M. Affenzeller and A. Ferscha and M. Haller and T. Jebelean and E.P. Klement and P. Paule and G. Pomberger and W. Schreiner and R. Stubenrauch and R. Wagner and G. Weiss and W. Windsteiger},

refereed = {no},

length = {39},

url = {http://www.springer.com/computer/programming/book/978-3-642-02126-8}

}

### Algorithms in Symbolic Computation

#### Peter Paule, Bruno Buchberger, Lena Kartashova, Manuel Kauers, Carsten Schneider, Franz Winkler

In: Hagenberg Research, Bruno Buchberger et al. (ed.), Chapter 1, pp. 5-62. 2009. Springer, 978-3-642-02126-8. [pdf]@

author = {Peter Paule and Bruno Buchberger and Lena Kartashova and Manuel Kauers and Carsten Schneider and Franz Winkler},

title = {{Algorithms in Symbolic Computation}},

booktitle = {{Hagenberg Research}},

language = {english},

chapter = {1},

pages = {5--62},

publisher = {Springer},

isbn_issn = {978-3-642-02126-8},

year = {2009},

annote = {2009-00-00-C},

editor = {Bruno Buchberger et al.},

refereed = {no},

length = {58}

}

**incollection**{RISC3845,author = {Peter Paule and Bruno Buchberger and Lena Kartashova and Manuel Kauers and Carsten Schneider and Franz Winkler},

title = {{Algorithms in Symbolic Computation}},

booktitle = {{Hagenberg Research}},

language = {english},

chapter = {1},

pages = {5--62},

publisher = {Springer},

isbn_issn = {978-3-642-02126-8},

year = {2009},

annote = {2009-00-00-C},

editor = {Bruno Buchberger et al.},

refereed = {no},

length = {58}

}

### Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs

#### N. Popov, T. Jebelean

Mathematics and Computers in Simulation 79(8), pp. 2293-2301. April 2009. Elsevier, ISSN: 0378-4754. [pdf]@

author = {N. Popov and T. Jebelean},

title = {{Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs}},

language = {english},

journal = {Mathematics and Computers in Simulation},

volume = {79},

number = {8},

pages = {2293--2301},

publisher = {Elsevier},

isbn_issn = {ISSN: 0378-4754},

year = {2009},

month = {April},

refereed = {yes},

length = {12}

}

**article**{RISC3095,author = {N. Popov and T. Jebelean},

title = {{Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs}},

language = {english},

journal = {Mathematics and Computers in Simulation},

volume = {79},

number = {8},

pages = {2293--2301},

publisher = {Elsevier},

isbn_issn = {ISSN: 0378-4754},

year = {2009},

month = {April},

refereed = {yes},

length = {12}

}

### Verification of Mutual Recursive Functional Programs

#### N. Popov, T. Jebelean

In: Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09, T. Ida, A. Bouhoula (ed.), pp. 120-122. September 2009. Carthage, Tunisia, .. [pdf]@

author = {N. Popov and T. Jebelean},

title = {{Verification of Mutual Recursive Functional Programs}},

booktitle = {{Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09}},

language = {english},

pages = {120--122},

address = {Carthage, Tunisia},

isbn_issn = {.},

year = {2009},

month = {September},

editor = {T. Ida and A. Bouhoula},

refereed = {yes},

length = {15}

}

**inproceedings**{RISC3912,author = {N. Popov and T. Jebelean},

title = {{Verification of Mutual Recursive Functional Programs}},

booktitle = {{Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09}},

language = {english},

pages = {120--122},

address = {Carthage, Tunisia},

isbn_issn = {.},

year = {2009},

month = {September},

editor = {T. Ida and A. Bouhoula},

refereed = {yes},

length = {15}

}

### Functional Program Verification in Theorema. Soundness and Completeness

#### N. Popov, T. Jebelean

In: Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09, J. Knoop, A. Prantl (ed.), pp. 221-229. October 2009. Maria Taferl, Austria, .. [pdf]@

author = {N. Popov and T. Jebelean},

title = {{Functional Program Verification in Theorema. Soundness and Completeness}},

booktitle = {{Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09}},

language = {english},

pages = {221--229},

address = {Maria Taferl, Austria},

isbn_issn = {.},

year = {2009},

month = {October},

editor = {J. Knoop and A. Prantl},

refereed = {yes},

length = {9}

}

**inproceedings**{RISC3913,author = {N. Popov and T. Jebelean},

title = {{Functional Program Verification in Theorema. Soundness and Completeness}},

booktitle = {{Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09}},

language = {english},

pages = {221--229},

address = {Maria Taferl, Austria},

isbn_issn = {.},

year = {2009},

month = {October},

editor = {J. Knoop and A. Prantl},

refereed = {yes},

length = {9}

}

### A Complete Method for Algorithm Validation

#### N. Popov, T. Jebelean

In: Proceedings of the Workshop on Automated Mathematical Theory Exploration AUTOMATHEO'09, B. Buchberger, R. McCasland, A. Craciun (ed.), pp. 21-25. June 2009. Hagenberg, Austria, -. [pdf]@

author = {N. Popov and T. Jebelean},

title = {{A Complete Method for Algorithm Validation}},

booktitle = {{Proceedings of the Workshop on Automated Mathematical Theory Exploration AUTOMATHEO'09}},

language = {english},

pages = {21--25},

address = {Hagenberg, Austria},

isbn_issn = {-},

year = {2009},

month = {June},

editor = {B. Buchberger and R. McCasland and A. Craciun},

refereed = {yes},

length = {5}

}

**inproceedings**{RISC3915,author = {N. Popov and T. Jebelean},

title = {{A Complete Method for Algorithm Validation}},

booktitle = {{Proceedings of the Workshop on Automated Mathematical Theory Exploration AUTOMATHEO'09}},

language = {english},

pages = {21--25},

address = {Hagenberg, Austria},

isbn_issn = {-},

year = {2009},

month = {June},

editor = {B. Buchberger and R. McCasland and A. Craciun},

refereed = {yes},

length = {5}

}

### 2008

### Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory

#### Adrian Craciun

Research Institute for Symbolic Computation (RISC). PhD Thesis. 2008. [pdf]@

author = {Adrian Craciun},

title = {{Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory}},

language = {english},

abstract = {This thesis is concerned with the implementation of the “lazy thinking” synthesis methodin the frame of the mathematical assistant system Theorema and its application to thesynthesis of algorithms in the theory of Gröbner bases. The “lazy thinking” method, proposed by Bruno Buchberger, the ﬁrst advisor of thisthesis, is part of his model of systematic theory exploration based on knowledge schemes.Essentially, lazy thinking is a deductive, scheme-based synthesis method: a proof of thecorrectness of an algorithm (i.e. its speciﬁcation) using an algorithm scheme and usingcomplete knowledge about the speciﬁcation is attempted. All deﬁnitions and propertiesof concepts involved in the speciﬁcations are known. The algorithm scheme is a deﬁnitionof the desired algorithm in terms of unknown subalgorithms. The proof is likely to fail,as no information about the unknown subalgorithms is available. Following an analysisof the failing proof, conjectures are generated and added to the knowledge, such that thefailure can be overcome. These conjectures turn out to be speciﬁcations for the unknownsubalgorithms. Algorithms that satisfy the generated speciﬁcations can then either beretrieved from the knowledge base, or synthesized by lazy thinking in subsequent roundsof exploration.We describe the method of lazy thinking and then describe its implementation in Theo-rema: • the cascade mechanism, that implements the lazy exploration cycles (initiate proof, proof failure analysis, conjecture generation), • failure analysis, and • conjecture generation.We then describe the usage of the cascade mechanism in conjunction with the reasonersavailable in the system. The problem of Gröbner bases represents a nontrivial benchmark for program synthesis.We present how, following an outline proposed by Bruno Buchberger, the lazy thinkingimplementation can be used in this case study. Starting from a critical-pair completionalgorithm scheme, we show how our implementation can be applied successfully to ef-fectively (re)invent the idea of S-polynomials (as outlined by Bruno Buchberger), andcomplete a proof of correctness.},

year = {2008},

translation = {0},

school = {Research Institute for Symbolic Computation (RISC)},

length = {157}

}

**phdthesis**{RISC3425,author = {Adrian Craciun},

title = {{Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory}},

language = {english},

abstract = {This thesis is concerned with the implementation of the “lazy thinking” synthesis methodin the frame of the mathematical assistant system Theorema and its application to thesynthesis of algorithms in the theory of Gröbner bases. The “lazy thinking” method, proposed by Bruno Buchberger, the ﬁrst advisor of thisthesis, is part of his model of systematic theory exploration based on knowledge schemes.Essentially, lazy thinking is a deductive, scheme-based synthesis method: a proof of thecorrectness of an algorithm (i.e. its speciﬁcation) using an algorithm scheme and usingcomplete knowledge about the speciﬁcation is attempted. All deﬁnitions and propertiesof concepts involved in the speciﬁcations are known. The algorithm scheme is a deﬁnitionof the desired algorithm in terms of unknown subalgorithms. The proof is likely to fail,as no information about the unknown subalgorithms is available. Following an analysisof the failing proof, conjectures are generated and added to the knowledge, such that thefailure can be overcome. These conjectures turn out to be speciﬁcations for the unknownsubalgorithms. Algorithms that satisfy the generated speciﬁcations can then either beretrieved from the knowledge base, or synthesized by lazy thinking in subsequent roundsof exploration.We describe the method of lazy thinking and then describe its implementation in Theo-rema: • the cascade mechanism, that implements the lazy exploration cycles (initiate proof, proof failure analysis, conjecture generation), • failure analysis, and • conjecture generation.We then describe the usage of the cascade mechanism in conjunction with the reasonersavailable in the system. The problem of Gröbner bases represents a nontrivial benchmark for program synthesis.We present how, following an outline proposed by Bruno Buchberger, the lazy thinkingimplementation can be used in this case study. Starting from a critical-pair completionalgorithm scheme, we show how our implementation can be applied successfully to ef-fectively (re)invent the idea of S-polynomials (as outlined by Bruno Buchberger), andcomplete a proof of correctness.},

year = {2008},

translation = {0},

school = {Research Institute for Symbolic Computation (RISC)},

length = {157}

}

### Multi-Domain Logic and its Applications to SAT

#### Tudor Jebelean, Gabor Kusper

In: SYNASC 2008, V. Negru et. al. (ed.), Proceedings of International Simposium on Symbolic and Numeric Scientific Computation, pp. 3-8. 2008. IEEE Society Press, 978-0-7695-3523-4. [pdf]@

author = {Tudor Jebelean and Gabor Kusper},

title = {{Multi-Domain Logic and its Applications to SAT}},

booktitle = {{SYNASC 2008}},

language = {English},

abstract = {We describe a new formalism and special proof methods for a novel generalization of propositional logic,which is especially suitable for solving the satisfiability problem (SAT).A Multi--Domain Logic (MDL) formula is quantifier--free and contains only atoms of the form $x \in A$,where $x$ is a variable and $A$ is a constant set.For formulae in conjunctive normal form, we are interested in finding solutions (assignments to variables which satisfy all clauses).Classical propositional logic corresponds to the special case when each set is either $\{\true\}$ or $\{\false\}$.The union of all the sets occurring for a certain variable can be seen as "the domain" of that variable, thus MDL is also a generalization of multi-valued logic, but with different domains for variables.The most distinctive feature is, however, the indication of the sub-domain in each clause.The notions of resolution, subsumption, as well as the basic steps of the DPLL method generalize in an elegant and straightforward way.As a novel MDL specific technique, {\em variable clustering} consists in creating a new variable ranging over the cartesian product of the domains of several "clustered" variables.This allows the transformation of classical SAT problems in MDL problems with less literals, and in which the propagation of information can be performed more efficiently than classical unit propagation.The basic idea of MDL originates from the earlier work of the second author on "hyper-unit" propagation (that is simultaneous propagation of several unit clauses) and on the representation and propagation of "k-literals" (generalized literals containing information on several propositional variables).Preliminary experiments with a prototype Java implementation exhibit speed--ups of up to 30 times.},

pages = {3--8},

publisher = {IEEE Society Press},

isbn_issn = {978-0-7695-3523-4},

year = {2008},

editor = {V. Negru et. al.},

refereed = {yes},

keywords = {Multi-Domain Logic, SAT, signed logic},

length = {6},

conferencename = {International Simposium on Symbolic and Numeric Scientific Computation}

}

**inproceedings**{RISC3949,author = {Tudor Jebelean and Gabor Kusper},

title = {{Multi-Domain Logic and its Applications to SAT}},

booktitle = {{SYNASC 2008}},

language = {English},

abstract = {We describe a new formalism and special proof methods for a novel generalization of propositional logic,which is especially suitable for solving the satisfiability problem (SAT).A Multi--Domain Logic (MDL) formula is quantifier--free and contains only atoms of the form $x \in A$,where $x$ is a variable and $A$ is a constant set.For formulae in conjunctive normal form, we are interested in finding solutions (assignments to variables which satisfy all clauses).Classical propositional logic corresponds to the special case when each set is either $\{\true\}$ or $\{\false\}$.The union of all the sets occurring for a certain variable can be seen as "the domain" of that variable, thus MDL is also a generalization of multi-valued logic, but with different domains for variables.The most distinctive feature is, however, the indication of the sub-domain in each clause.The notions of resolution, subsumption, as well as the basic steps of the DPLL method generalize in an elegant and straightforward way.As a novel MDL specific technique, {\em variable clustering} consists in creating a new variable ranging over the cartesian product of the domains of several "clustered" variables.This allows the transformation of classical SAT problems in MDL problems with less literals, and in which the propagation of information can be performed more efficiently than classical unit propagation.The basic idea of MDL originates from the earlier work of the second author on "hyper-unit" propagation (that is simultaneous propagation of several unit clauses) and on the representation and propagation of "k-literals" (generalized literals containing information on several propositional variables).Preliminary experiments with a prototype Java implementation exhibit speed--ups of up to 30 times.},

pages = {3--8},

publisher = {IEEE Society Press},

isbn_issn = {978-0-7695-3523-4},

year = {2008},

editor = {V. Negru et. al.},

refereed = {yes},

keywords = {Multi-Domain Logic, SAT, signed logic},

length = {6},

conferencename = {International Simposium on Symbolic and Numeric Scientific Computation}

}

### A Prototype Environment for Verification of Recursive Programs

#### N. Popov, T. Jebelean

In: FORMED'08, Z. Istenes (ed.), Proceedings of Formal Methods in Computer Science Education, Budapest, Hungary, ENTCS , pp. 121-130. March 2008. Elsevier, .. [pdf]@

author = {N. Popov and T. Jebelean},

title = {{A Prototype Environment for Verification of Recursive Programs}},

booktitle = {{FORMED'08}},

language = {english},

series = {ENTCS},

pages = {121--130},

publisher = {Elsevier},

isbn_issn = {.},

year = {2008},

month = {March},

editor = {Z. Istenes},

refereed = {yes},

length = {10},

conferencename = {Formal Methods in Computer Science Education, Budapest, Hungary}

}

**inproceedings**{RISC3399,author = {N. Popov and T. Jebelean},

title = {{A Prototype Environment for Verification of Recursive Programs}},

booktitle = {{FORMED'08}},

language = {english},

series = {ENTCS},

pages = {121--130},

publisher = {Elsevier},

isbn_issn = {.},

year = {2008},

month = {March},

editor = {Z. Istenes},

refereed = {yes},

length = {10},

conferencename = {Formal Methods in Computer Science Education, Budapest, Hungary}

}