Back
Publications of Volker Sorge (ordered by type/date)
Please respect possible copyrights.
Edited Books
- Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakzu Suzuki, and Freek Wiedijk, eds.
Intelligent Computer Mathematics -- Joint Proceedings of AISC 2008, Calculemus 2008 and MKM 2008
LNAI 5144, Springer Verlag.
- Weixiong Zhang and Volker Sorge, eds.
Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems
Frontiers in AI and Application, IOS Press, 2004.
(Available at Amazon)
- Jacques Calmet and Belaid Benhamou and Olga Caprotti and Laurent Henocque and Volker Sorge, eds.
Artificial Intelligence, Automated Reasoning, and Symbolic Computation --- Joint International Conference, AISC 2002 and Calculemus 2002
LNAI 2385, Springer Verlag.
(BibTeX)
Book Chapters
- Andreas Meier and Volker Sorge
Applying SAT solving in classification of finite algebras
Satisfiability Research in the Year 2005.
Springer Verlag, 2006, ISBN 1-4020-4552-2.
(PostScript, pdf)
- Christoph Benzmüller and Andreas Meier and Volker Sorge
Bridging theorem proving and mathematical knowledge retrieval
Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, 2005.
pp. 277-296, LNAI 2605, Springer Verlag.
(PostScript, pdf, BibTeX)
Articles in Journals
- Volker Sorge, Andreas Meier, Roy McCasland, and Simon Colton
Automatic Construction and Verification of Isotopy Invariants
Journal of Automated Reasoning40(2-3):221243, 2008.
(PostScript, pdf)
- Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber
Can a Higher-Order and a First-Order Theorem Prover Cooperate?
Journal of Applied Logic6:318342, 2008.
(PostScript, pdf)
- Volker Sorge and Simon Colton and Roy McCasland and Andreas Meier
Classification Results in Quasigroup and Loop Theory via a Combination of Automated Reasoning Tools
Commentationes Mathematicae Universitatis Carolinae49(2-3):319340, 2008.
(PostScript, pdf)
- Andreas Meier and Volker Sorge
Applying SAT solving in classification of finite algebras
Journal of Automated Reasoning, 35(1-3):201-235, 2005.
(PostScript, pdf)
- Olga Caprotti and Volker Sorge
Editorial: Integration of automated reasoning and computer algebra systems
Journal of Symbolic Computation, 39(5):501--502, May 2005.
- Andreas Meier and Martin Pollet and Volker Sorge
Comparing Approaches to the Exploration of the Domain of Residue Classes
Journal of Symbolic Computation, 34(4), 2002.
(PostScript, pdf, BibTeX)
- J. Siekmann, S. Hess, C. Benzmüller, L. Cheikhrouhou, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, M.Pollet, V. Sorge
LOUI: Lovely Omega User Interface
Formal Aspects of Computing, 11(3), 1999.
(gzipped PostScript, pdf, BibTeX)
- Christoph Benzmüller, Matthew Bishop, Volker Sorge
Integrating TPS and OMEGA
Journal of Universal Computer Science, 5(3), 1999.
(Online Version, BibTeX, PostScript, pdf)
- A. Franke, S. Hess, Ch. Jung, M. Kohlhase and V. Sorge
Agent-Oriented Integration of Distributed Mathematical Services
Journal of Universal Computer Science, 5(3), 1999.
(Online Version, BibTeX, PostScript, pdf)
- J. Siekmann, H. Horacek, M. Kohlhase, C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, S. Hess, K. Konrad, A. Meier, E. Melis, V. Sorge
An Interactive Proof Development Environment + Anticipation = A Mathematical Assistant?
International Journal of Computing Anticipatory Systems (CASYS), 3, pages 101-110.
- Manfred Kerber, Michael Kohlhase, Volker Sorge
Integrating Computer Algebra into Proof Planning
Journal of Automated Reasoning, 21(3), 1998.
(PostScript, pdf, BibTeX)
Refereed Conference/Workshop Proceedings
- Alan Sexton, Volker Sorge, and Stephen M. Watt
Computing with Abstract Matrix Structures
Proceedings of International Symposium on Symbolic and Algebraic Computation, ISSAC'2009.
ACM Press.
(PostScript, pdf)
- Josef Baker and Alan Sexton and Volker Sorge
A Linear Grammar Approach to Mathematical Formula Recognition from PDF
Mathematical Knowledge Management, 8th International Conference, MKM 2008.
LNCS 5625, Springer Verlag, 2009.
(PostScript, pdf)
- Alan P. Sexton and Volker Sorge and Stephen M. Watt
Reasoning with Generic Cases in the Arithmetic of Abstract Matrices
Proceedings of the Calculemus Symposium 2009.
LNCS 5625, Springer Verlag, 2009.
(PostScript, pdf)
- Joseph Baker, Alan Sexton, and Volker Sorge
An Online Repository of Mathematical Samples
Proceedings of Workshop on Digital Mathematical Libraries 2009.
Masaryk University Publications.
(PostScript, pdf)
- Alan Sexton, Volker Sorge, and Stephen M. Watt
Abstract Matrix Arithmetic
Proceedings of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing -- SYNASC-2008.
IEEE Computer Society Press.
(PostScript, pdf)
- Joseph Baker, Alan Sexton, and Volker Sorge
Extracting Precise Data from PDF Documents
Proceedings of Workshop on Digital Mathematical Libraries 2008.
Masaryk University Publications.
(PostScript, pdf)
- Simon Colton and Volker Sorge
Automated Parameterisation of Finite Algebras
Workshop on Empirical Successful Automated Reasoning in Mathematics, 2008.
(PostScript, pdf)
- Jacques Carette and William M. Farmer and Volker Sorge
A Rational Reconstruction of a System for Experimental Mathematics
Proceedings of the Calculemus Symposium 2007.
pp. 13--26, LNCS 4108, Springer Verlag.
(PostScript, pdf)
- Arithmetic on Matrices with Blocks of Symbolic Size
Alan P. Sexton, Volker Sorge, and Stephen M. Watt
ISSAC 2007 poster abstracts, ACM Commun. Comput. Algebra.
ACM.
(PostScript, pdf)
- Catriona Kennedy and Georgios Theodoropoulos and Volker Sorge and Edward Ferrari and Peter Lee and Chris Skelcher
AIMSS: An Architecture for Data Driven Simulations in the Social Sciences
Computational Science - ICCS 2007, 7th International Conference, 2007.
pp. 1098--1105, LNCS 4108, Springer Verlag.
- Volker Sorge and Andreas Meier and Roy McCasland and Simon Colton
Automatic Construction and Verification of Isotopy Invariants
Automated Reasoning --- 3rd International Joint Conference, IJCAR 2006.
pp. 36--51, LNAI 4130, Springer Verlag.
(PostScript, pdf)
- Alan Sexton and Volker Sorge
Abstract Matrices in Symbolic Computation
Proceedings of International Symposium on Symbolic and Algebraic Computation, ISSAC'2006.
pp.318--325, ACM Press.
(PostScript, pdf)
- Simon Colton and Pedro Torres and Paul Cairns and Volker Sorge
Managing Automatically Formed Mathematical Theories
Mathematical Knowledge Management, 5th International Conference, MKM 2006.
LNCS 4108, Springer Verlag, 2006.
(PostScript, pdf)
- Amar Raja, Matthew Rayner, Alan Sexton, and Volker Sorge
Towards a Parser for Mathematical Formula Recognition
Mathematical Knowledge Management, 5th International Conference, MKM 2006.
LNCS 4108, Springer Verlag, 2006.
(PostScript, pdf)
- Toshihiro Kanahori, Alan Sexton, Volker Sorge, and Masakazu Suzuki
Capturing Abstract Matrices from Paper
Mathematical Knowledge Management, 5th International Conference, MKM 2006.
pp. 139--151, LNCS 4108, Springer Verlag, 2006.
(PostScript, pdf)
- Volker Sorge and Andreas Meier and Roy McCasland and Simon Colton
Integrating AI Systems for Classification in Non-associative Algebra
Proceedings of the Calculemus Symposium 2006.
Electronic Notes in Theoretical Computer Science, Elsevier.
(PostScript, pdf)
- Frank Theiß, Volker Sorge, and Martin Pollet
Interfacing to Computer Algebra via Term Indexing
Proceedings of the Calculemus Symposium 2006.
Electronic Notes in Theoretical Computer Science, Elsevier.
(PostScript, pdf)
- Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber
Can a higher-order and a first-order theorem prover cooperate
Proceedings of 11th LPAR, 2005.
LNCS 3452, Springer Verlag.
(PostScript, pdf)
- Andreas Meier and Volker Sorge
A new set of algebraic benchmark problems for sat solvers
8th International Conference, SAT 2005.
pp.459-466, LNCS 3569, Springer Verlag.
(PostScript, pdf)
- Martin Pollet and Volker Sorge
Connecting logical representations and efficient computations
Proceedings of the Calculemus Symposium 2005.
pp.127-142, Electronic Notes in Theoretical Computer Science 151(1), Elsevier, 2006.
(PostScript, pdf)
- Alan Sexton and Volker Sorge
Semantic analysis of matrix structures
International Conference in Document Analysis and Recognition, 2005.
pp. 1141-1145, IEEE Computer Society Press.
(PostScript, pdf)
- Alan Sexton and Volker Sorge
Processing textbook-style matrices
Mathematical Knowledge Management, 4th International Conference, MKM 2005.
pp. 111--125, LNCS 3863, Springer Verlag, 2006.
(PostScript, pdf)
- Alan Sexton and Volker Sorge
A database of glyphs for OCR of mathematical documents
Mathematical Knowledge Management, 4th International Conference, MKM 2005.
LNCS 3863, Springer Verlag, 2006.
(PostScript, pdf)
- Martin Pollet and Volker Sorge
Towards an efficient representation of computational objects
Proceedings of the 5th Workshop on the Implementation of Logics.
ULCS-05-003 Technical Report, University of Liverpool.
(PostScript, pdf)
- Simon Colton and Andreas Meier and Volker Sorge and Roy McCasland
Automatic Generation of Classification Theorems for Finite Algebras
Automated Reasoning --- 2nd International Joint Conference, IJCAR 2004.
LNAI 3097, Springer Verlag.
(PostScript, pdf, BibTeX)
- Volker Sorge and Simon Colton and Andreas Meier and Roy McCasland
A Grid-based Application of Machine Learning to Model Generation
KI 2004: Advances in artificial intelligence : Joint German/Austrian Conference on AI, Work in Progress Papers.
(PostScript, pdf)
- Martin Pollet and Volker Sorge and Manfred Kerber
Intuitive and Formal Representations: The Case of Matrices
Mathematical Knowledge Management, Third International Conference, MKM 2004.
LNAI 3119, Springer Verlag.
(PostScript, pdf)
- Helmut Horacek and Armin Fiedler and Andreas Franke and Markus Moschner and Martin Pollet and Volker Sorge
Representation of Mathematical Concepts for Inferencing and for Presentation Purposes
Proceedings of the 17th European Meeting on Cybernetics and Systems Research.
(PostScript)
- Martin Pollet and Volker Sorge
Integrating Computational Properties at the Term Level
Proceedings of the Calculemus Symposium 2003.
Aracne, Roma.
(PostScript, pdf)
- Arjeh Cohen and Scott H. Murray and Martin Pollet and Volker Sorge
Certifying Solutions to Permutation Group Problems
Proceedings of the 19th Conference on Automated Deduction (CADE-19), 2003.
LNAI 2741, Springer Verlag.
(PostScript, pdf)
- Andreas Meier and Volker Sorge and Simon Colton
Employing Theory Formation to Guide Proof Planning
Proceedings of the Calculemus Symposium 2002.
LNAI 2385, Springer Verlag.
(PostScript, pdf, BibTeX)
- J. Siekmann and C. Benzmüller and V. Brezhnev and L. Cheikhrouhou and A. Fiedler and A. Franke and H. Horacek and M. Kohlhase and A. Meier and E. Melis and M. Moschner and I. Normann and M. Pollet and V. Sorge and C. Ullrich and C.-P. Wirth and J. Zimmer
Proof Development with OMEGA
Proceedings of the 18th Conference on Automated Deduction (CADE-18), 2002.
LNAI 2392, Springer Verlag.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Andreas Meier and Volker Sorge
Distributed Assertion Retrieval
First International Workshop on Mathematical Knowledge Management RISC-Linz, 2001.
(PostScript, pdf, BibTeX)
- Andreas Meier and Martin Pollet and Volker Sorge
Classifying Isomorphic Residue Classes
Proceedings of the 8th International Workshop on Computer Aided Systems Theory (EuroCAST 2001).
LNCS 2178, Springer Verlag.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Mateja Jamnik and Manfred Kerber and Volker Sorge
Experiments with an Agent-Oriented Reasoning System
Proceedings of Joint German/Austrian Conference on AI, 2001.
LNAI 2174, Springer Verlag.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Mateja Jamnik and Manfred Kerber and Volker Sorge
An Agent-oriented Approach to Reasoning
Proceedings of the Calculemus Symposium 2001.
(PostScript, pdf, BibTeX)
- Andreas Meier and Volker Sorge
Exploring Properties of Residue Classes
Proceedings of the Calculemus Symposium 2000.
AK Peters, 2001.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Volker Sorge
OANTS - An open approach at combining Interactive and Automated Theorem Proving
Proceedings of the Calculemus Symposium 2000.
AK Peters, 2001.
(PostScript, pdf, BibTeX)
- Lassaad Cheikhrouhou and Volker Sorge
PDS - A Three-Dimensional Data Structure for Proof Plans
Proceedings of the International Conference on Artificial and Computational Intelligence (ACIDCA'2000), 2000.
(PostScript, pdf, BibTeX)
- Volker Sorge
Non-Trivial Symbolic Computations in Proof Planning
Proceedings of FroCoS`2000.
LNCS 1794, Springer Verlag.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Volker Sorge
Critical Agents Supporting Interactive Theorem Proving
Proceedings of 9th Portuguese Conference on Artificial Intelligence (EPIA-99), 1999.
LNAI 1695, Springer Verlag.
(PostScript, pdf, BibTeX)
- Erica Melis and Volker Sorge
Employing External Reasoners in Proof Planning
7th CALCULEMUS Workshop.
Electronic Notes in Theoretical Computer Science 23(3), Elsevier.
(PostScript, pdf, BibTeX)
- C. Benzmüller, M. Jamnik, M. Kerber, V. Sorge
Agent Based Mathematical Reasoning
7th CALCULEMUS Workshop, 1999.
Electronic Notes in Theoretical Computer Science 23(3), Elsevier.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Volker Sorge
A Blackboard Architecture for Guiding Interactive Proofs
Proceedings of 8th International Conference AIMSA'98, 1998.
LNAI 1480, Springer Verlag.
(PostScript, pdf, BibTeX)
- S. Hess, Ch. Jung, M. Kohlhase, V. Sorge
An Implementation of Distributed Mathematical Services
6th CALCULEMUS and TYPES Workshop, 1998.
(PostScript, pdf, BibTeX)
- J. Siekmann, H. Horacek, M. Kohlhase, C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, S. Hess, K. Konrad, A. Meier, E. Melis, V. Sorge
An Interactive Proof Development Environment + Anticipation = A Mathematical Assistant?
Proceedings of the 2nd International Conference CASYS'98, 1998.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Volker Sorge
Integrating TPS with OMEGA
work in progress paper, TPHOLs '98 (see Technical Report 98-08,
Department of Computer Science, The Australian National University).
Also available in Proceedings of Workshop "Inference Mechanisms in Knowledge-Based
Systems: Theory and Applications, KI '98, Bremen, 1998.".
(gzipped PostScript, pdf, BibTeX)
- C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, V. Sorge
Omega: Towards a Mathematical Assistant
in Proceedings of the 14th Conference on Automated Deduction (CADE-14), 1997.
LNAI 1249, Springer Verlag.
(PostScript, pdf, BibTeX)
- Manfred Kerber, Michael Kohlhase, Volker Sorge
Integrating Computer Algebra with Proof Planning
in Proceedings of the International Symposium DISCO '96 .
LNCS 1128, Springer Verlag.
(PostScript, pdf, BibTeX)
Non-refereed Conference/Workshop Proceedings
- Alan Sexton and Volker Sorge
Database-driven Mathematical Character Recognition
In Proceedings of Graphics Recognition, Algorithms and Applications, GREC 2005.
LNCS, Springer Verlag, 2006.
(PostScript, pdf)
- Frank Theiß and Volker Sorge
Automatic Generation of Algorithms and Tactics
Work in progress paper: Calculemus 2002.
(PostScript, pdf, BibTeX)
- Armin Fiedler and Andreas Franke and Helmut Horacek and Markus Moschner and Martin Pollet and Volker Sorge
Ontological Issues in the Representation and Presentation of Mathematical Concepts
ECAI-15 Workshop: Ontologies and Semantic Interoperability, 2002.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Andreas Meier and Erica Melis and Martin Pollet and Jörg Siekmann and Volker Sorge
Proof Planning: A Fresh Start?
Proceedings of the IJCAR 2001 Workshop: Future Directions in Automated Reasoning, 2001.
(PostScript, pdf, BibTeX)
- Andreas Meier and Volker Sorge
Exploring the Domain of Residue Classes
Workshop on The Role of Automated Deduction in Mathematics at CADE-17, 2000.
(PostScript, pdf, BibTeX)
- Lassaad Cheikhrouhou and Volker Sorge
Planning Equivalence Proofs
Workshop on Using AI Methods in Deduction at CADE-15, 1998.
(PostScript, pdf, BibTeX)
- J. Siekmann, S. Hess, C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, V. Sorge
LOUI: A Distributed Graphical User Interface for the Interactive Proof System OMEGA
4th Workshop UITP-98, 1998.
(gzipped PostScript, pdf, BibTeX)
- Volker Sorge
Towards a Translation of Computer Algebra Algorithms into Tactics
in Proceedings of the 1st Workshop on Abstraction, Analogy and Metareasoning, 1996.
(PostScript, pdf, BibTeX)
Theses
- Volker Sorge
A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning
PhD Thesis, 2001.
(gzipped PostScript, pdf, BibTeX)
- Volker Sorge
Einbindung eines Computeralgebrasystems in eine logische Beweisumgebung
Masters Thesis, 1996.
(PostScript, pdf, BibTeX)
Abstracts
- Quratul-ain Mahesar and Volker Sorge
Classification of Quasigroup-structures with respect to their Cryptographic Properties
Proceedings of the 16th Workshop on Automated
Reasoning: Bridging the Gap between Theory and Practice, 2009.
(PostScript, pdf)
- Josef Baker, Alan Sexton, and Volker Sorge
Extracting Precise Data from PDF Documents for Mathematical Formula Recognition
In 8th IAPR International Workshop on Document Analysis Systems, Extended Abstracts, 2008.
(PostScript, pdf)
- Alan P. Sexton and Volker Sorge
Reasoning on Abstract Matrix Structures
Proceedings of the 15th Workshop on Automated
Reasoning: Bridging the Gap between Theory and Practice, 2008.
(PostScript, pdf)
- Jacques Carette and William M. Farmer and Volker Sorge
A Rational Reconstruction of a System for Experimental Mathematics
Proceedings of the 14th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2007.
(PostScript, pdf)
- Volker Sorge
Managing Mathematical Workflows
Proceedings of the 13th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2006.
(PostScript, pdf)
- Alan Sexton and Volker Sorge
Abstract matrices and constraints
Proceedings of the 12th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2005.
(PostScript, pdf)
- Simon Colton and Andreas Meier and Volker Sorge and Roy McCasland
Automatic Generation of Classification Theorems for Finite Algebras
Proceedings of the 11th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2004.
(PostScript, pdf)
- Roy McCasland and Volker Sorge
Automating Algebra's Tedious Tasks: Computerised Classification
Workshop on Challenges and Novel Applications for Automated Reasoning at CADE-19, 2003.
(PostScript, pdf)
- Arjeh Cohen and Scott H. Murray and Martin Pollet and Volker Sorge
Proof Planning some Permutation Group Problems
Proceedings of the 10th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2003.
(PostScript, pdf)
- Christoph Benzmüller and Volker Sorge
Agent-based Theorem Proving
Proceedings of the 9th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2002.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Andreas Meier and Martin Pollet and Volker Sorge
Proof expansion and transformation with a parameterisable inference machine
Proceedings of the Eighth Workshop on Automated Reasoning, Bridging the Gap between
Theory and Practice, 2001.
(PostScript, pdf, BibTeX)
- C. Benzmüller, M. Jamnik, M. Kerber, V. Sorge
Resource Guided Concurrent Deduction
extended abstract, Seventh Workshop on Automated Reasoning Bridging the Gap between Theory and Practice, London, July 2000.
(PostScript, pdf, BibTeX)
- J. Siekmann, C. Benzmüller, A. Fiedler, A. Franke, H. Horacek,P. Libbrecht, M. Kohlhase, A. Meier, E. Melis, M. Pollet, V. Sorge, C. Ullrich, J. Zimmer
Adaptive Course Generation and Presentation
Proceedings of ITS-2000 workshop on Adaptive and Intelligent Web-Based Education Systems, 2000.
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Volker Sorge
Towards Fine-Grained Proof Planning with Critical Agents
extended abstract, Sixth Workshop on Automated Reasoning Bridging the Gap between Theory and Practice in conjunction with AISB'99 Convention, Edinburgh, April 1999.
(PostScript, pdf, BibTeX)
Technical Reports
- Andreas Meier and Martin Pollet and Volker Sorge
Classifying Residue Classes --- Results of a Case Study
Seki-Report SR-01-01, December 2001.
(BibTeX)
- Andreas Meier and Martin Pollet and Volker Sorge
Exploring the Domain of Residue Classes
Seki-Report SR-00-04, December 2000.
(PostScript, pdf, BibTeX)
- Erica Melis and Volker Sorge
Specialized External Reasoners in Proof Planning
Seki-Report SR-00-01, January 2000.
(PostScript, pdf, BibTeX)
- C. Benzmüller, M. Jamnik, M. Kerber, and V. Sorge
Towards Concurrent Resource Managed Deduction
Seki-Report SR-99-07, November 1999
Also appeared as Cognitive Science Research Paper TR-CSRP-99-17,
School of Computer Science and Cognitive Science Research Centre,
The University of Birmingham (UK), November 1999..
(PostScript, pdf, BibTeX)
- Christoph Benzmüller and Volker Sorge
Resource Adaptive Agents in Interactive Theorem Proving
Seki-Report SR-99-02, March 1999.
(PostScript, pdf, BibTeX)
- Manfred Kerber, Michael Kohlhase, Volker Sorge
An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs
Seki-Report SR-96-06, 1996.
(PostScript, pdf, BibTeX)
Back