The SFB program expired on September 30, 2008. For the link to the successor project click DK Computational Mathematics

Technical Reports

Publication Lists

Annual Reports

Publications of the Project F1302


Article


September 27, 2008

Bibliography

1

B. Buchberger.
Automated Theorem Proving: Theory or Practice?
Mitteilungen der Deutschen Mathematiker-Vereinigung, 2, 2000.

2

B. Buchberger.
Mathematics and computer science - a personal view.
An. Mat. Univ. Timisoara, 24(1):3-18, 2000.
ISSN 1224-970X.

3

B. Buchberger.
Mathematik am Computer: Die nächste Überforderung? (Mathematics on the Computer: The Next Overtaxation?).
Didaktikreihe der österreichischen mathematischen Gesellschaft, 131:37-56, March 2000.

4

B. Buchberger.
Gröbner bases and systems theory.
Journal of Multidimensional Systems and Signal Processing, 12(3-4):223-251, 2001.

5

B. Buchberger.
Theorema: A short introduction.
Mathematica Journal, 8(2):247-252, 2001.
ISSN 1047-5974.

6

B. Buchberger.
Algorithm Invention and Verification by Lazy Thinking.
Analele Universitatii din Timisoara, Seria Matematica - Informatica, XLI:41-70, 2003.
special issue on Computer Science - Proceedings of SYNASC'03.

7

B. Buchberger.
Towards the automated synthesis of a Gröbner Bases algorithm.
RACSAM - Revista de la Real Academia de Ciencias (Review of the Spanish Royal Academy of Science), Serie A: Mathematicas, 98(1):65-75, 2004.

8

B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger.
Theorema: Towards computer-aided mathematical theory exploration.
Journal of Applied Logic, 4(4):470-504, 2006.

9

B. Buchberger and T. Jebelean.
Teaching of mathematics using Theorema.
International Journal of Computer Algebra in Mathematical Education, 6(1):25-50, 1999.

10

M. Giese.
Superposition-based equality handling for analytic tableaux.
Journal of Automated Reasoning, 38(1-3):127-153, December 2006.
Appeared online 2 December 2006, in print April 2007.

11

T. Ida and B. Buchberger.
Proving and Solving in Computational Origami.
Analele Universitatii din Timisoara, Seria Matematica - Informatica, XLI:247-263, 2003.
special issue on Computer Science - Proceedings of SYNASC'03.

12

T. Jebelean, L. Kovacs, and N. Popov.
Experimental program verification in the Theorema system.
STTT, 2006.
in press.

13

L. Kovacs and T. Jebelean.
Practical Aspects of Imperative Program Verification in Theorema.
Analele Universitatii din Timisoara, Seria Matematica - Informatica, XLI:135-154, 2003.
special issue on Computer Science - Proceedings of SYNASC'03.

14

L. Kovacs and T. Jebelean.
Automated generation of loop invariants by recurrence solving in Theorema.
Analele Universitatii din Timisoara, Seria Matematica - Informatica, XLII:151-166, 2004.
special issue on Computer Science - Proceedings of SYNASC'04.

15

L. Kovacs, N. Popov, and T. Jebelean.
Verification environment in Theorema.
Annals of Mathematics, Computing and Teleinformatics (AMCT), 1(2):27-34, 2005.

16

G. Kusper.
Solving the resolution-free sat problem by hyper-unit propagation in linear time.
Annals of Mathematics and Artificial Intelligence, 43(1-4):129-136, 2005.

17

T. Kutsia.
Pattern unification with sequence variables and flexible arity symbols.
Electronic Notes in Theoretical Computer Science, 66(5), 2002.

18

T. Kutsia.
Context sequence matching for XML.
Electronic Notes in Theoretical Computer Science, 157(2):47-65, 2006.

19

T. Kutsia.
Solving equations with sequence variables and sequence functions.
JSC, 43(2):352-388, 2007.

20

M. Marin and T. Kutsia.
Foundations of the rule-based system rholog.
Journal of Applied Non-Classical Logics, 16(1-2):151-168, 2006.

21

K. Nakagawa.
Logicographic symbols.
Journal of Symbolic Computation: Special Issue, 2003.

22

N. Popov and T. Jebelean.
Using computer algebra techniques for the specification, verification and synthesis of recursive programs.
Mathematics and Computers in Simulation, pages 1-13, 2007.
to appear.

23

M. Rosenkranz.
Symbolic solution of simple BVPs on the operator level.
SIGSAM Bulletin, 37(3):84-87, 2003.

24

M. Rosenkranz.
New symbolic method for solving linear two-point boundary value problems on the level of operators.
Journal of Symbolic Computation, 39(2):171-199, 2004.

25

S. Saminger, R. Vajda, and W. Windsteiger.
Using a computer-algebra system and a theorem prover to stimulate creativity in learning mathematics.
International Journal of Computers for Mathematical Learning, 2005.
Submitted.

26

R. Vajda, T. Jebelean, and B. Buchberger.
Combining Logical and Algebraic Techniques for Natural Style Proving in Elementary Analysis.
Mathematics and Computers in Simulation, pages 1-11, 2007.
to appear.

27

W. Windsteiger.
An automated prover for Zermelo-Fraenkel set theory in Theorema.
JSC, 41(3-4):435-470, 2006.

Please direct your comments or eventual problem reports to webmaster.
SpezialForschungsBereich SFB F013 | Special Research Program of the FWF - Austrian Science Fund