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

InProceedingsReferred - 2007

September 27, 2008


B. Beckert, M. Giese, R. Hähnle, V. Klebanov, P. Rümmer, S. Schlager, and P. H. Schmitt.
The key system 1.0 (deduction component).
In F. Pfenning, editor, Proceedings, International Conference on Automated Deduction, Bremen, Germany, volume 4603 of LNCS, pages 1-6. Springer, 2007.
A. Craciun and M. Hodorog.
Decompositions of Natural Numbers: From A Case Study in Mathematical Theory Exploration.
In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors, Proceedings of the 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'07), pages 1-8, Timisoara, Romania, 26-29 September 2007.
to appear as IEEE volume.
L. Kovacs.
Aligator: a Package for Reasoning about Loops.
In Proc. of 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Yerevan, Armenia, October 2007.
Short paper. to appear.
L. Kovacs.
Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema.
In M. Giese and T. Jebelean, editors, Proc. of WING'07, RISC, Austria, pages 56-69, 2007.
RISC Report Series No. 07-07.
T. Kutsia, J. Levy, and M. Villaret.
Sequence unification through currying.
In F. Baader, editor, Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA'07), volume 4533 of Lecture Notes in Computer Science, pages 288-302, Paris, France, 2007.
G. Mayrhofer, S. Saminger, and W. Windsteiger.
Creacomp: Computer-supported experiments and automated proving in learning and teaching mathematics.
In E. Milkova, editor, Proceedings of ICTMT8, Hradec Kralove, Czech Republic, July 2007.
G. Mayrhofer, S. Saminger, and W. Windsteiger.
Creacomp: Experimental formal mathematics for the classroom.
In D. Wang, editor, SCE'06 book. World Scientific, 2007.
Accepted for publication.
N. Popov and T. Jebelean.
Proving termination of recursive programs by matching against simplified program versions and construction of specialized libraries in Theorema.
In D. Hofbauer and A. Serebrenik, editors, Proceedings of 9-th International Workshop on Termination, pages 48-52, Paris, France, June 2007.
J. Robu.
Automated proof of geometry theorems involving order relation in the frame of the Theorema project.
In H. F. Pop, editor, Knowledge Engineering: Principles and Techniques, number Special Issue in Studia Universitatis ``Babes-Bolyai'', Series Informatica, pages 307-315, 2007.

Please direct your comments or eventual problem reports to webmaster.

SpezialForschungsBereich SFB F013 | Special Research Program of the FWF - Austrian Science Fund