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

Technical Reports

Publication Lists

Annual Reports


Publications of the Project F1302


InProceedingsReferred


September 27, 2008

Bibliography

1
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.
2
B. Buchberger.
Theory exploration versus theorem proving.
In A. Armando and T. Jebelean, editors, Electronic Notes in Theoretical Computer Science, volume 23. Elsevier, 1999.
CALCULEMUS Workshop, University of Trento, Trento, Italy.
3
B. Buchberger.
Mathematica and computer science: A personal view.
In T. Jebelean and V. Negru, editors, Proceedings of the Second International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, (SYNASC'00), Timisoara, Romania, October 2000.
4
B. Buchberger.
Theorema Proving For and With Gröbner Bases.
In K. Galkowski and E. Rogers, editors, Proceedings of the Second International Workshop on Multidimensional (nD) Systems, June 27-30, Czocha Castle, Poland, pages 15-22, 2000.
5
B. Buchberger.
Theory exploration with Theorema.
In T. Jebelean and V. Negru, editors, Proceedings of the Second International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'00), Timisoara, Romania, October 2000.
6
B. Buchberger.
Gröbner Bases: A Short Introduction for Systems Theorists.
In R. Moreno-Diaz, B. Buchberger, and J. L. Freire, editors, EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), number 2201 in Lecture Notes in Computer Science, pages 1-19, Las Palmas de Gran Canaria, February 19-23 2001. Springer.
ISSN 0302-9743, ISBN 3-540-42959-X.
7
B. Buchberger.
Logicographic symbols: A new feature in Theorema.
In Symbolic Computation - New Horizons (Proceedings of the 4th International Mathematica Symposium), pages 23-30, Tokyo Denki University, Chiba Campus, Japan, June 25 - 27 2001. Tokyo Denki University Press.
ISBN 4-501-73020-X C3041.
8
B. Buchberger.
The PCS prover in Theorema.
In R. Moreno-Diaz, B. Buchberger, and J. L. Freire, editors, EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), number 2201 in Lecture Notes in Computer Science, pages 469-478, Las Palmas de Gran Canaria, Feb. 19-23 2001. Springer.
ISSN 0302-9743, ISBN 3-540-42959-X.
9
B. Buchberger.
Theorema: Extending Mathematica by automated proving.
In D. Bosanac and D. Ungar, editors, PrimMath 2001 (The Programming System Mathematica in Science, Technology, and Education), pages 10-11. University of Zagreb, September 27-28 2001.
ISBN 953-6076-71-3.
10
B. Buchberger.
Invention by Lazy Thinking.
In R. Wagner, editor, ``A Min Tjoa @ Work''- In honor of the 50th birthday of Univ.Prof.Dr. A Min Tjoa, pages 11-31. Austrian Computer Society, December 2002.
11
B. Buchberger.
Algorithm supported mathematical theory exploration: A personal view and stragegy.
In B. Buchberger and J. Campbell, editors, Proceedings of AISC 2004 (7 th International Conference on Artificial Intelligence and Symbolic Computation), volume 3249 of Springer Lecture Notes in Artificial Intelligence, pages 236-250. Copyright: Springer, Berlin-Heidelberg, 22-24 September 2004.
12
B. Buchberger, K. Aigner, C. Dupre, T. Jebelean, F. Kriftner, M. Marin, K. Nakagawa, O. Podisor, E. Tomuta, Y. Usenko, D. Vasaru, and W. Windsteiger.
Theorema: An Integrated System for Computation and Deduction in Natural Style.
In Proceedings of CADE 98 (International Conference on Computer Aided Deduction), Lindau, Germany, July 5-10, 1998.
Workshop on integration of proving and computing.
13
B. Buchberger and A. Craciun.
Algorithm synthesis by lazy thinking: Examples and implementation in Theorema.
In F. Kamareddine, editor, Electronic Notes in Theoretical Computer Science, volume 93, pages 24-59, 18 February 2004.
Proc. of the Mathematical Knowledge Management Workshop, Edinburgh, Nov. 25, 2003.
14
B. Buchberger and A. Craciun.
Algorithm synthesis by lazy thinking: Using problem schemes.
In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors, Proceedings of 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04), pages 90-106, Timisoara, Romania, 26-30 September 2004. Mirton Publisher.
15
B. Buchberger, C. Dupré, T. Jebelean, K. Kriftner, K. Nakagawa, D. Vasaru, and W. Windsteiger.
The Theorema project: A progress report.
In M. Kerber and M. Kohlhase, editors, Proceedings of the 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, St. Andrews, Scotland, pages 100-115, August 2000.
16
B. Buchberger and T. Ida.
Computational origami: Interaction of solving, proving and computing.
In Proceedings of World Conference on 21st Century Mathematics, Lahore, Pakistan, 18-20 March 2004.
17
B. Buchberger and T. Jebelean.
Distance teaching of mathematics using Theorema.
In H. Gutmann, editor, Proceedings of the Third Technion Symposium on Software for Communication, Hagenberg, Austria, April 1999.
18
B. Buchberger, T. Jebelean, and D. Vasaru.
Theorema: A System for Formal Scientific Training in Natural Language Presentation.
In Proceedings of ED-MEDIA 98 (International Conference on Educational Multimedia), Freiburg, Germany, pages 174-179, June 20-23 1998.
19
B. Buchberger and K. Nakagawa.
Logicographic symbols: A new concept in logic syntax.
In Proceedings of the INTAS Conference on Rewriting Techniques and Efficient Theorem Proving, 2000.
20
B. Buchberger, D. Vasaru, and T. Jebelean.
The Theorema system: Current status and the proving-solving-computing cycle.
In Proceedings of RTETP (Rewriting Techniques and Efficient Theorem Proving), Kiev, June 2000.
21
B. Buchberger and W. Windsteiger.
The Theorema Language: Implementing Object- and Meta-Level Usage of Symbols.
In Proceedings of Calculemus 98, Eindhoven, Netherlands, 1998.
22
E. M. Clarke, A. S. Gavlovski, K. Sutner, and W. Windsteiger.
Analytica V: Towards the Mordell-Weil Theorem.
In A. Bigatti and S. Ranise, editors, Proceedings of Calculemus'06, Genova, Italy, 2006.
23
A. Craciun and B. Buchberger.
Proving the correctness of the merge-sort algorithm with Theorema.
In Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'02), pages 97-111, Timisoara, Romania, October 2002.
ISBN 973-585-785-5.
24
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.
25
M. Giese.
Saturation up to redundancy for tableau and sequent calculi.
In M. Hermann and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 13th Intl. Conf., LPAR 2006, Phnom Penh, Cambodia, volume 4246 of LNCS, pages 182-196, 2006.
26
M. Hodorog and A. Craciun.
Scheme-Based Systematic Exploration of Natural Numbers.
In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors, Proceedings of the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06), Timisoara, Romania, pages 23-34, 26-29 September 2006.
27
T. Ida and M. Marin.
Functional Logic Origami Programming with Open CFLP.
In P. Mitic, P. Ramsden, and J. Carne, editors, Challenging the Boundaries of Symbolic Computation. Proceedings of 5th International Mathematica Symposium (IMS 2003), Imperial College, London, 2003. Imperial College Press.
28
T. Ida, M. Marin, and H. Takahashi.
Constraint Functional Logic Programming for Origami Construction.
In Proceedings of the First Asian Symposium on Programming Languages and Applications, Beijing, China, 2003.
29
T. Ida, D. Tepeneu, B. Buchberger, and J. Robu.
Proving and constraint solving in computational origami.
In B. Buchberger and J. Campbell, editors, Proceedings of AISC 2004 (7 th International Conference on Artificial Intelligence and Symbolic Computation), volume 3249 of Springer Lecture Notes in Artificial Intelligence, pages 132-142. Copyright: Springer-Berlin, 22-24 September 2004.
30
T. Jebelean.
Nonconventional Algorithms for Multiprecision Arithmetic.
In V. Negru et al., editors, Proceeding of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'02), pages 3-7, Timisoara, Romania, October 2002. Mirton.
31
T. Jebelean and B. Konev.
Using meta-variables for natural deduction in Theorema.
In M. Kerber and M. Kohlhase, editors, Proceedings of the CALCULEMUS 2000 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, pages 160-175, St. Andrews, Scotland, August 6-7 2000.
32
T. Jebelean, L. Kovacs, and N. Popov.
Verification of imperative programs in Theorema.
In D. Dranidis and K. Tigka, editors, Proceedings of the 1st South-East European Workshop in Formal Methods (SEEFM'03), Thessaloniki, Greece, November 20 2003.
33
T. Jebelean, L. Kovacs, and N. Popov.
Experimental program verification in the Theorema system.
In T. Margaria and B. Steffen, editors, Proceedings ISOLA 2004, pages 92-99, Paphos, Cyprus, November 2004.
34
T. Jebelean and L. Szakacs.
Functional-based synthesis of systolic online multipliers.
In D. Zaharie, D. Petcu, V. Negru, and T. Jebelean, editors, International Symposium on Symbolic and Numeric Scientific Computing (SYNASC'05), Timisoara, Romania, pages 267-275. IEEE Computer Society, 2005.
35
N. Kobayashi, M. Marin, and T. Ida.
A web oriented system for equational solving.
In G. Vidal, editor, Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming, WFLP'03, 2003.
36
B. Konev and T. Jebelean.
Combining level-saturation strategies and meta-variables for predicate logic proving in Theorema.
In IMACS ACA 2000, St. Petersburg, Russia, June 2000.
37
B. Konev and T. Jebelean.
Solution Lifting Method for Handling Meta-variables in Theorema.
In V. Negru and T. Jebelean, editors, 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01), Timisoara, Romania, October 2001.
38
F. Kossak and K. Nakagawa.
User System Interaction Within Theorema.
In A. Armando and T. Jebelean, editors, Electronic Notes in Theoretical Computer Science, volume 23. Elsevier, 1999.
Calculemus 99 Workshop, Trento, Italy.
39
A. Kovacs and L. Kovacs.
The lagrange interpolation formula in determining the fluid's velocity potential through profile grids.
In F. Fazekas et al., editors, Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-147/148, Balatonalmadi, Hungary, 26-29 May 2005. Technical University of Budapest, PAMM-Centre.
40
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.
41
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.
42
L. Kovacs and T. Jebelean.
Generation of Invariants in Theorema.
In N. Boja, editor, Proceedings of the 10th International Symphosium of Mathematics and its Application, pages 407-415, 6-9 November 2003.
Scientific Bulletins of the Politehnica University Timisoara, Transactions on Mathematics and Physics.
43
L. Kovacs and T. Jebelean.
Practical aspects of imperative program verification using Theorema.
In T. Jebelean and V. Negru, editors, Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03), Timisoara, Romania, 2003.
44
L. Kovacs and T. Jebelean.
Automated generation of loop invariants by recurrence solving in Theorema.
In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors, Proceedings of the 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04), pages 451-464, Timisoara, Romania, 26-30 September 2004. Mirton Publisher.
45
L. Kovacs and T. Jebelean.
Generation of loop invariants in Theorema by combinatorial and algebraic methods.
In F. Fazekas et al., editors, Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-144, volume vol. CVI, pages 125-134, Balatonalmadi, Hungary, 20-23 May 2004. Technical University of Budapest, PAMM-Centre.
46
L. Kovacs and T. Jebelean.
An algorithm for automated generation of invariants for loops with conditionals.
In T. Jebelean and V. Negru, editors, 7th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), Timisoara, Romania, pages 16-19, September 25-28 2005.
47
L. Kovacs and T. Jebelean.
Finding polynomial invariants for imperative loops in the Theorema system.
In S. Autexier and H. Mantel, editors, Proceedings of Verify'06 Workshop, IJCAR'06, The 2006 Federated Logic Conference, Seattle, USA, pages 52-67, August 15-16 2006.
48
L. Kovacs, T. Jebelean, and A. Kovacs.
Practical aspects of algebraic invariant generation for loops with conditionals.
volume CVIII/2251, pages 116-125. Technical University of Budapest, PAMM-Centre, 2005.
ISSN 0133-3526. Proc. of Pannonian Applied Mathematical Meetings, PC-147/148, Balatonalmadi, Hungary, 26-29 May 2005.
49
L. Kovacs, N. Popov, and T. Jebelean.
Combining logic and algebraic techniques for program verification in Theorema.
In T. Margaria and B. Steffen, editors, Proceedings ISOLA 2006, Paphos, Cyprus, November 2006.
50
F. Kriftner.
Theorema: The Language.
In B. Buchberger and T. Jebelean, editors, Proceedings of the Second International Theorema Workshop, Hagenberg, Austria, pages 39-54, 1998.
available as RISC report 98-10.
51
G. Kusper.
Integrating Temporal Assertions into a Parallel Debugger.
In B. Monien and R. Feldmann, editors, Proceedings of the 8th International Euro-Par Conference, pages 113-120, Paderborn, Germany, 2002. Springer-Verlag.
52
T. Kutsia.
Theorem proving with sequence variables and flexible arity symbols.
In M. Baaz and A. Voronkov, editors, Logic in Programming, Artificial Intelligence and Reasoning. Proceedings of the 9th International Conference LPAR'02, volume 2514 of Lecture Notes in Artificial Intelligence, pages 278-291, Tbilisi, Georgia, October 14-18 2002. Springer Verlag.
ISBN 3-540-00010-0.
53
T. Kutsia.
Unification with sequence variables and flexible arity symbols and its extension with pattern-terms.
In J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, editors, Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proceedings of Joint AICS'2002 - Calculemus'2002 conference, volume 2385 of Lecture Notes in Artificial Intelligence, pages 290-304, Marseille, France, July 2002. Springer Verlag.
ISBN 3-540-43865-3.
54
T. Kutsia.
Equational prover of Theorema.
In R. Nieuwenhuis, editor, Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03), volume 2706 of LNCS, Valencia, Spain, 2003. Springer Verlag.
55
T. Kutsia.
Matching in flat theories.
In J. Levy, M. Kohlhase, J. Niehren, and M. Villaret, editors, Proceedings of the 17th International Workshop on Unification (UNIF 2003), Valencia, Spain, 2003.
56
T. Kutsia.
Unification modulo flatness.
In T. Jebelean and V. Negru, editors, Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03), Timisoara, Romania, 2003.
57
T. Kutsia.
Solving equations involving sequence variables and sequence functions.
In B. Buchberger and J. A. Campbell, editors, Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Computation, AISC'04, volume 3249 of Lecture Notes in Artificial Intelligence, pages 157-170, Hagenberg, Austria, Sep 22-24 2004. Springer Verlag.
58
T. Kutsia.
Context sequence matching for XML.
In M. Alpuente, S. Escobar, and M. Falaschi, editors, Proceedings of the 1th International Workshop on Automated Specification and Verification of Web Sites (WWV'05), pages 103-119, Valencia, Spain, March 14-15 2005.
(Final version to appear in Elsevier ENTCS).
59
T. Kutsia and B. Buchberger.
Predicate logic with sequence variables and sequence function symbols.
In A. Asperti, G. Bancerek, and A. Trybulec, editors, Proceedings of the 3rd International Conference on Mathematical Knowledge Management, MKM'04, volume 3119 of Lecture Notes in Computer Science, pages 205-219, Bialowieza, Poland, Sep 19-21 2004. Springer Verlag.
60
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.
61
T. Kutsia and M. Marin.
Unification procedure for terms with sequence variables and sequence functions (extended abstract).
In M. Kohlhase, editor, Proceedings of the 18th International Workshop on Unification (UNIF'04), pages 1-13, Cork, Ireland, 5 2004.
62
T. Kutsia and M. Marin.
Can context sequence matching be used for querying XML?
In L. Vigneron, editor, Proceedings of the 19th International Workshop on Unification (UNIF'05), pages 77-92, Nara, Japan, 2005.
63
T. Kutsia and M. Marin.
Matching with regular constraints.
In G. Sutcliffe and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 12th International Conference LPAR'05, volume 3835 of Lecture Notes in Artificial Intelligence, pages 215-229, Montego Bay, Jamaica, 2005. Springer Verlag.
64
T. Kutsia and M. Marin.
Solving regular constraints for hedges and contexts.
In J. Levy, editor, Proceedings of 20th International Workshop on Unification, UNIF'06, pages 89-107, Seattle, USA, 2006.
65
M. Marin.
Functional programming with sequence variables: The sequentica package.
In J. Levy, M. Kohlhase, J. Niehren, and M. Villaret, editors, Proceedings of the 17th International Workshop on Unification (UNIF 2003), 2003.
66
M. Marin and T. Kutsia.
On the implementation of a rule-based programming system and some of its applications.
In B. Konev and R. Schmidt, editors, Proceedings of the Fourth International Workshop on the Implementation of Logics, Almaty, Kazakhstan, 2003.
67
M. Marin and T. Kutsia.
Programming with transformation rules.
In T. Jebelean and V. Negru, editors, Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03), Timisoara, Romania, 2003.
68
M. Marin and T. Kutsia.
A rule-based approach to the implementation of evaluation strategies.
In D. Petcu, D. Zaharie, V. Negru, and T. Jebelean, editors, Proceedings of the 6th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04), pages 227-241, Timisoara, Romania, Sep 26-30 2004. Mirton Publishing Company.
69
M. Marin and F. Piroi.
Deduction and presentation in ${\rho}$log.
In F. Kamareddine, editor, Proceedings of the Mathematical Knowledge Management Symposium, volume 93 of ENTCS, pages 161-182. Heriot-Watt University, Edinburgh, Elsevier, February 2004.
70
M. Marin and F. Piroi.
Rule-based programming with mathematica.
In Proceedings of the 6th International Mathematica Conference, Alberta, Canada. Wolfram Institute, August 2004.
Also as RICAM report series 2004-16.
71
M. Marin and D. Tepeneu.
Programming with Sequence Variables: The Sequentica Package.
In P. Mitic, P. Ramsden, and J. Carne, editors, Challenging the Boundaries of Symbolic Computation. Proceedings of 5th International Mathematica Symposium (IMS 2003), Imperial College, London, 2003. Imperial College Press.
72
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.
73
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.
74
K. Nakagawa.
Variable Shape Logicographic Symbols.
In K. Nakagawa, editor, Logic, Mathematics and Computer Science: Interactions (LMCS 2002), pages 202-216, RISC, Schloss Hagenberg, Austria, October 2002.
75
K. Nakagawa and B. Buchberger.
Two tools for mathematical knowledge management in Theorema.
In B. Buchberger and O. Caprotti, editors, First International Workshop on Mathematical Knowledge Management (MKM 2001), Schloss Hagenberg, Austria, RISC, September 2001. RISC-Linz.
ISBN 3-902276-00-2.
76
F. Piroi.
Focus windows: A tool for automated provers.
In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors, Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'02), Timisoara, Romania, October 2002.
ISBN 973-585-785-5.
77
F. Piroi.
User interface features in Theorema: A summary.
In P. Libbrecht, editor, In Proceedings of ``Mathematical User-Interfaces Workshop'' At the Third Mathematical Knowledge Management Conference, Bialowieza, Poland, pages 1-16, 2004.
Also available as SFB Technical Report 2004-46.
78
F. Piroi and B. Buchberger.
Focus windows: A new technique for proof presentation.
In J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, editors, Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proceedings of Joint AICS'2002 - Calculemus'2002 Conference., volume 2385 of Lecture Notes in Artificial Intelligence, pages 290-304, Marseille, France, July 2002. Springer Verlag.
ISBN 3-540-43865-3.
79
F. Piroi and B. Buchberger.
Focus Windows: A New Technique for Proof Presentation.
In H. Kredel and W. Seiler, editors, Proceedings of the 8th Rhine Workshop on Computer Algebra, Mannheim, Germany, pages 297-313, March 21-22 2002.
80
F. Piroi and B. Buchberger.
An environment for building mathematical knowledge libraries.
In W. Windsteiger and C. Benzmueller, editors, Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, Second International Joint Conference (IJCAR), pages 19-29, Cork, Ireland, 4-8 July 2004.
81
F. Piroi and B. Buchberger.
Label management in Theorema.
In M. Kohlhase, editor, Informal proceedings of the 4th International Conference on Mathematical Knowledge Management (MKM'05), July 2005.
Bremen, Germany.
82
F. Piroi and T. Jebelean.
Advanced Proof Presentation in Theorema.
In V. Negru and T. Jebelean, editors, 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01), Timisoara, Romania, October 2001.
83
F. Piroi and T. Kutsia.
The Theorema environment for interactive proof development.
In G. Sutcliffe and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 12th International Conference (LPAR'05), volume 3835 of Lecture Notes in Artificial Intelligence, pages 261-275, Montego Bay, Jamaica, 2005. Springer Verlag.
84
N. Popov and T. Jebelean.
A practical approach to verification of recursive programs in Theorema.
In T. Jebelean and V. Negru, editors, Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03), Timisoara, Romania, 2003.
85
N. Popov and T. Jebelean.
A practical approach to proving termination of recursive programs in Theorema.
In M. Codish and A. Middeldorp, editors, Proceedings of 7th International Workshop on Termination, pages 43-46, Aachen, Germany, June 2004.
86
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.
87
J. Robu.
Systematic Exploration of Geometric Configurations Using Mathematica.
In V. Negru and T. Jebelean, editors, 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01), Timisoara, Romania, October 2001.
88
J. Robu.
Systematic exploration of geometric configurations using Mathematica.
In Analele Universitatii Timisoara, volume XXXIX of Seria Matematica-Informatica, pages 209-216, Timisoara, Romania, 2002.
89
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.
90
J. Robu, D. Tepeneu, T. Ida, H. Takahashi, and B. Buchberger.
Computational origami construction of a regular heptagon with automated proof of its correctness.
In H. Hong and D. Wang, editors, Proceedings of ADG 2004 (The Fifth International Workshop on Automated Deduction in Geometry), volume 3763 of Lecture Notes in Computer Science, pages 19-33. University of Florida, Gainesville, FL, USA, Springer Berlin / Heidelberg, 2006.
91
M. Rosenkranz.
Symbolic solution of simple BVPs on the operator level: A new approach.
In T. Jebelean and V. Negru, editors, Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03), Timisoara, Romania, 2003.
92
M. Rosenkranz.
The algorithmization of physics: Math between science and engineering.
In B. Buchberger and J. A. Campbell, editors, Proceedings of AISC 2004, volume 3249 of Lecture Notes in Artificial Intelligence (LNAI), pages 1-7, Castle of Hagenberg, Austria, September 2004. Springer.
Invited talk.
93
M. Rosenkranz, B. Buchberger, and H. W. Engl.
Solving Linear Boundary Value Problems Via Non-commutative Gröbner Bases.
In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors, Proceedings of SYNASC 2002, 4th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, pages 300-313, Timisoara, Romania, 9-12 October 2002. Mirton Publisher.
94
E. Tomuta and B. Buchberger.
Combining Provers in the Theorema System.
In Proceedings of the Sixth Rhine Workshop on Computer Algebra, March 31.-April 3, Sankt Augustin, Germany, 1998.
95
W. Windsteiger.
Building up Hierarchical Mathematical Domains Using Functors in Mathematica.
In A. Armando and T. Jebelean, editors, Electronic Notes in Theoretical Computer Science, volume 23. Elsevier, 1999.
Calculemus 99 Workshop, Trento, Italy.
96
W. Windsteiger.
On a solution of the mutilated checkerboard problem using the Theorema set theory prover.
In S. Linton and R. Sebastiani, editors, Proceedings of the Calculemus 2001 Symposium, 2001.
Talk given at the Calculemus 2001 workshop, June 21, 2001.
97
W. Windsteiger.
An Automated Prover for Set Theory in Theorema.
In O. Caprotti and V. Sorge, editors, Calculemus 2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning: Work in Progress Papers, pages 56-67, Marseille, France, June 2002.
Appears in Seki-Report Series Nr. SR-02-04, Universität des Saarlandes.
98
W. Windsteiger.
An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema.
In K. Nakagawa, editor, Logic, Mathematics and Computer Science: Interactions (LMCS 2002), pages 266-280, RISC, Schloss Hagenberg, Austria, October 2002.
Symposium in Honor of Bruno Buchberger's 60th Birthday, Appears in RISC-report Series Nr. 02-60.
99
W. Windsteiger.
Exploring an algorithm for polynomial interpolation in the Theorema system.
In T. Hardin and R. Rioboo, editors, Calculemus 2003. 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, pages 130-136. Aracne, 2003.




Please direct your comments or eventual problem reports to webmaster.

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