PROVE Project: Interactive Software for Mathematical Proof Learning [PROVE]

Project Description

Projektkosten: ATS 4.700.000

Project Lead

Project Duration

01/04/1998 - 31/03/2001

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.
[bib]
@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.
[bib]
@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}
}

2001

A Set Theory Prover in Theorema

W. Windsteiger

In: Computer Aided Systems Theory, R. Moreno-Diaz and B. Buchberger and J.L. Freire (ed.), LNCS 2178, pp. 525-539. 2001. Springer, ISSN 0302-9743, ISBN 3-540-429. Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), extended version available as RISC report 01-07.
[bib]
@inproceedings{RISC169,
author = {W. Windsteiger},
title = {{A Set Theory Prover in Theorema}},
booktitle = {{Computer Aided Systems Theory}},
language = {english},
series = {LNCS},
number = {2178},
pages = {525--539},
publisher = {Springer},
isbn_issn = {ISSN 0302-9743, ISBN 3-540-429},
year = {2001},
note = {Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory -- Formal Methods and Tools for Computer Science), extended version available as RISC report 01-07},
editor = {R. Moreno-Diaz and B. Buchberger and J.L. Freire},
refereed = {yes},
length = {15}
}

On a Solution of the Mutilated Checkerboard Problem using the Theorema Set Theory Prover

W. Windsteiger

In: Proceedings of the Calculemus 2001 Symposium, S. Linton and R. Sebastiani (ed.), pp. 28-47. 2001. [pdf]
[bib]
@inproceedings{RISC170,
author = {W. Windsteiger},
title = {{On a Solution of the Mutilated Checkerboard Problem using the Theorema Set Theory Prover}},
booktitle = {{Proceedings of the Calculemus 2001 Symposium}},
language = {english},
pages = {28--47},
isbn_issn = {?},
year = {2001},
editor = {S. Linton and R. Sebastiani},
refereed = {yes},
length = {20}
}

A Set Theory Prover in Theorema: Implementation and Practical Applications

Wolfgang Windsteiger

RISC Institute. PhD Thesis. May 2001. [tar.gz]
[bib]
@phdthesis{RISC312,
author = {Wolfgang Windsteiger},
title = {{A Set Theory Prover in Theorema: Implementation and Practical Applications}},
language = {english},
year = {2001},
month = {May},
translation = {0},
school = {RISC Institute},
length = {248}
}

A Set Theory Prover within Theorema

Wolfgang Windsteiger

Technical report no. 01-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. February 2001. Also available as SFB report 01-23. [ps]
[bib]
@techreport{RISC1527,
author = {Wolfgang Windsteiger},
title = {{A Set Theory Prover within Theorema}},
language = {english},
number = {01-07},
year = {2001},
month = {February},
note = {Also available as SFB report 01-23},
keywords = {Automated Theorem Proving, Theorema},
sponsor = {FWF project F1302 (SFB Numerical and Symbolic Scientific Computing).},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

2000

The Theorema System: Proving, Solving, and Computing for the Working Mathematician

B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger

Technical report no. 00-38 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. August 2000. [ps]
[bib]
@techreport{RISC1518,
author = {B. Buchberger and C. Dupre and T. Jebelean and B. Konev and F. Kriftner and T. Kutsia and K. Nakagawa and F. Piroi and D. Vasaru and W. Windsteiger},
title = {{The Theorema System: Proving, Solving, and Computing for the Working Mathematician}},
language = {english},
number = {00-38},
year = {2000},
month = {August},
annote = {2000-00-38-A},
sponsor = {FWF SFB P1302, INTAS 76-960, Land Oberösterreich},
length = {5},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

The Natural Style Provers of Theorema: A Survey of Strategies for Different Mathematical Domains

B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger

Technical report no. 00-39 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. June 2000. [ps]
[bib]
@techreport{RISC1519,
author = {B. Buchberger and C. Dupre and T. Jebelean and B. Konev and F. Kriftner and T. Kutsia and K. Nakagawa and F. Piroi and D. Vasaru and W. Windsteiger},
title = {{The Natural Style Provers of Theorema: A Survey of Strategies for Different Mathematical Domains}},
language = {english},
number = {00-39},
year = {2000},
month = {June},
annote = {2000-00-39-A},
sponsor = {FWF SFB P1302, INTAS 76-960, Land Oberösterreich},
length = {3},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

The Facilities of Theorema for Teaching Logic and Mathematics

B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger

Technical report no. 00-41 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. June 2000. [ps]
[bib]
@techreport{RISC1521,
author = {B. Buchberger and C. Dupre and T. Jebelean and B. Konev and F. Kriftner and T. Kutsia and K. Nakagawa and F. Piroi and D. Vasaru and W. Windsteiger},
title = {{The Facilities of Theorema for Teaching Logic and Mathematics}},
language = {english},
number = {00-41},
year = {2000},
month = {June},
annote = {2000-00-41-A},
sponsor = {FWF SFB P1302, INTAS 76-960, Land Oberösterreich},
length = {4},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

1999

Theorema: A Progress Report

Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger

Technical report no. 99-42 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. December 1999. Also available as SFB Report 99-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999. [ps]
[bib]
@techreport{RISC1479,
author = {Bruno Buchberger and Claudio Dupre and Tudor Jebelean and Franz Kriftner and Koji Nakagawa and Daniela Vasaru and Wolfgang Windsteiger},
title = {{Theorema: A Progress Report}},
language = {english},
number = {99-42},
year = {1999},
month = {December},
annote = {1999-12-00-C},
note = {Also available as SFB Report 99-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999},
keywords = {automatic reasoning},
sponsor = {SFB/FWF project F1302},
length = {11},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Theorema: A Short Demo

Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger

Technical report no. 99-45 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. December 1999. Also available as SFB Report 99-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999. [tar.gz]
[bib]
@techreport{RISC1481,
author = {Bruno Buchberger and Claudio Dupre and Tudor Jebelean and Franz Kriftner and Koji Nakagawa and Daniela Vasaru and Wolfgang Windsteiger},
title = {{Theorema: A Short Demo}},
language = {english},
number = {99-45},
year = {1999},
month = {December},
annote = {1999-12-00-C},
note = {Also available as SFB Report 99-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999},
keywords = {automated reasoning},
sponsor = {SFB/FWF project F1302},
length = {61},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Building Up Hierarchical Mathematical Domains Using Functors in THEOREMA

Windsteiger W.

In: Electronic Notes in Theoretical Computer Science, A. Armando and T. Jebelean (ed.), Proceedings of Calculemus'99, Trento, Italy, ENTCS 23/3, pp. 401-419. 1999. Elsevier, ISSN: 1571-0661. [url] [pdf]
[bib]
@inproceedings{RISC153,
author = {Windsteiger W.},
title = {{Building Up Hierarchical Mathematical Domains Using Functors in THEOREMA}},
booktitle = {{Electronic Notes in Theoretical Computer Science}},
language = {english},
series = {ENTCS},
volume = {23},
number = {3},
pages = {401--419},
publisher = {Elsevier},
isbn_issn = {ISSN: 1571-0661},
year = {1999},
editor = {A. Armando and T. Jebelean},
refereed = {yes},
length = {19},
conferencename = {Calculemus'99, Trento, Italy},
url = {http://www.elsevier.com/locate/entcs/volume23.html}
}

Theorema: Overview on Using the System and Details on Composing Hierarchical Knowledge Bases

Wolfgang Windsteiger

Technical report no. 99-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. June 1999. Presented at the Edinburgh School in Logic and Computation. [tar.gz]
[bib]
@techreport{RISC1338,
author = {Wolfgang Windsteiger},
title = {{Theorema: Overview on Using the System and Details on Composing Hierarchical Knowledge Bases}},
language = {english},
number = {99-15},
year = {1999},
month = {June},
note = {Presented at the Edinburgh School in Logic and Computation},
keywords = {automatic reasoning},
sponsor = {Austrian Science Fundation (FWF), SFB project P1302 (Theorema)},
length = {0},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

1998

Theorema: An Integrated System for Computation and Deduction in Natural Style

Bruno Buchberger, Klaus Aigner, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Mircea Marin, Koji Nakagawa, Ovidiu Podisor, Elena Tomuta, Yaroslav Usenko, Daniela Vasaru, Wolfgang Windsteiger

Technical report no. 98-25 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. December 1998. Also available as SFB Report No. 98-06. [ps]
[bib]
@techreport{RISC1432,
author = {Bruno Buchberger and Klaus Aigner and Claudio Dupre and Tudor Jebelean and Franz Kriftner and Mircea Marin and Koji Nakagawa and Ovidiu Podisor and Elena Tomuta and Yaroslav Usenko and Daniela Vasaru and Wolfgang Windsteiger},
title = {{Theorema: An Integrated System for Computation and Deduction in Natural Style}},
language = {english},
number = {98-25},
year = {1998},
month = {December},
annote = {1998-07-00-A},
note = {Also available as SFB Report No. 98-06},
keywords = {automated reasoning},
sponsor = {Austrian Science Foundation (FWF), project FO-1302 (SFB)},
length = {7},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

The Theorema Language: Implementing Object- and Meta-Level Usage of Symbols

B. Buchberger, W. Windsteiger

SFB F013 Numerical and Symbolic Scientific Computing. Technical report no. 98-07, 1998. [pdf]
[bib]
@techreport{RISC2144,
author = {B. Buchberger and W. Windsteiger},
title = {{The Theorema Language: Implementing Object- and Meta-Level Usage of Symbols}},
language = {english},
number = {98-07},
year = {1998},
annote = {1998-07-00-B},
institution = {SFB F013 Numerical and Symbolic Scientific Computing},
length = {12}
}

The Theorema Language: Implemening Object- and Meta-Level Usage of Symbols

B. Buchberger, W.Windsteiger

In: Proceedings of the Second International Theorema Workshop, B. Buchberger, T. Jebelean (ed.), pp. -. June 29-30 1998. RISC, Hagenberg, Austria, -. RISC-Linz Report Series No. 98-10.
[bib]
@inproceedings{RISC2417,
author = {B. Buchberger and W.Windsteiger},
title = {{The Theorema Language: Implemening Object- and Meta-Level Usage of Symbols}},
booktitle = {{Proceedings of the Second International Theorema Workshop}},
language = {english},
pages = { --},
address = {RISC, Hagenberg, Austria},
isbn_issn = {-},
year = {1998},
month = {June 29-30},
annote = {1998-06-29-E},
note = {RISC-Linz Report Series No. 98-10},
editor = {B. Buchberger and T. Jebelean},
refereed = {no},
length = {11}
}

Loading…