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

1999

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

1998

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…