Publications
Disclaimer: This site contains postscript and PDF files of articles that may be covered by copyright. You may browse the articles at your convenience (in the same spirit as you may read a journal or a proceeding article in a public library). Retrieving, copying, distributing these files may violate the copyright protection law.
- Articles in Journals
2008
2006
- Jörg Siekmann, Christoph Benzmüller, and Serge Autexier. Computer Supported Mathematics with OMEGA, Journal of Applied Logic, special issue on Mathematics Assistance Systems 4(4), December, 2006 Paper
(local copy)
Bib
- Mossakowski, Till, Autexier, Serge, and Hutter, Dieter. Development Graphs - Proof Management for Structured Specifications, Journal of Logic and Algebraic Programming, special issue on Algebraic Specification and Development Techniques 67(1-2), p. 114-145, April, 2006 (local copy)
Bib
2000
- Autexier, S., Hutter, D., Langenstein, B., Mantel, H., Rock, G., Schairer, A., Stephan, W., Vogt, R., and Wolpers, A.. VSE: Formal methods meet industrial needs, International Journal on Software Tools for Technology Transfer, Special issue on Mechanized Theorem Proving for Technology 3(1), September, 2000 Bib
- Chapters in Books
2010
- Serge Autexier, Dieter Hutter, and Till Mossakowski. Change Management for Heterogeneous Development Graphs, In Simon Siegler and Nathan Wasser (Ed) Verification, Induction, Termination Analysis, Festschrift in honor of Christoph Walther, LNCS, Springer, November, 2010 (local copy)
Bib
2009
- Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, and Serge Autexier. Jacques Herbrand: Life, Logic, and Automated Deduction, In Logic from Russell to Church, Vol. 5, Handbook of The History of Logic, Elsevier, p. 195-254, June, 2009 Bib
- Serge Autexier , Christoph Benzmüller, Dominik Dietrich, and Jörg Siekmann. Resource Adaptive Processes in Automated Reasoning Systems, In Matthew Crocker and Jörg Siekmann (Ed) Resource Adaptive Cognitive Processes, Part III – Resource-Adaptive Rationality in Machines , LNAI, Springer, p. 389-423, 2009 Paper
(local copy)
Bib
2007
- Jörg Siekmann and Serge Autexier. Computer Supported Formal Work: Towards a Digital Mathematical Assistant, In Roman Matuszewski and Anna Zalewska (Ed) From insight to proof - Jubilee Book for Andrzej Trybulec, Vol. 10(23), Studies in Logic, Grammar and Rhetoric, University of Bialystok, p. 231-248, July, 2007 Paper
Bib
- Roy McCasland, Alan Bundy, and Serge Autexier. Automated Discovery of Inductive Theorems, In Roman Matuszewski and Anna Zalewska (Ed) From insight to proof - Jubilee Book for Andrzej Trybulec, Vol. 10(23), Studies in Logic, Grammar and Rhetoric, University of Bialystok, p. 135-150, July, 2007 Bib
2006
- Serge Autexier, Christoph Benzmüller, Armin Fiedler, Henri Lesourd. Integrating Proof Assistants as Plugins in a Scientific Editor, In Michael Kohlhase (Ed) OMDOC - An Open Markup Format for Mathematical Documents [Version 1.2], Vol. 4180, LNAI, Springer, p. 309-312, August, 2006 Bib
- Serge Autexier, Dieter Hutter, Till Mossakowski, Axel Schairer. MAYA: Maintaining Structured Developments, In Michael Kohlhase (Ed) OMDOC - An Open Markup Format for Mathematical Documents [Version 1.2], Vol. 4180, LNAI, Springer, p. 281-285, August, 2006 Bib
2005
- Autexier, Serge and Hutter, Dieter. Formal Software Development in Maya, In Hutter, Dieter and Stephan, Werner (Ed) Festschrift in Honor of J. Siekmann, Vol. 2605, LNAI, Springer, February, 2005 Paper
(local copy)
Bib
2004
- Till Mossakowski, Piotr Hoffman, Serge Autexier, and Dieter Hutter. Part IV: CASL Logic, In Mosses, Peter D. (Ed) CASL Reference Manual , Vol. 2960, LNCS, Springer, p. 275-362, 2004 Paper
Bib
- Edited Proceedings and Special Issues
2010
- Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton(Ed) Proceedings of Conferences on Intelligent Computer Mathematics 2010 (CICM 2010) , Vol. 6167, LNCS, Springer, CNAM, Paris, France, July, 2010 Paper
Bib
- Serge Autexier, Petr Sojka, and Masakazu Suzuki(Ed) Special Issue on Authoring, Digitalization and Management of Mathematical Knowledge, Vol. 3, Nr. 3 of Journal Mathematics in Computer Science, Birkhäuser Basel, May, 2010 Paper
Bib
2008
- Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow(Ed) Special Issue on Formal Modeling and Verification of Critical Systems, Vol. forthcoming, Springer, December, 2008 Bib
- Serge Autexier and Christoph Benzmüller(Ed) Proceedings of the 8th Workshop on User Interfaces for Theorem Provers (UITP'08), Vol. forthcoming, Montréal, Canada, August, 2008 Bib
- Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, and Freek Wiedijk(Ed) Intelligent Computer Mathematics, Vol. 5144, LNAI, Springer, Birmingham, UK, July, 2008 Bib
2006
- Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm and Pierre Wolper(Ed) Proceedings of the Workshop "Trustworthy Software" 2006, Dagstuhl Research Online Publication Server, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, September, 2006 Paper
Bib
- Serge Autexier and Heiko Mantel(Ed) Proceedings of the 3rd Verification Workshop (VERIFY'06), Seattle, WA, USA, August, 2006 Bib
- Serge Autexier and Christoph Benzmüller(Ed) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP'06), Seattle, WA, USA, August, 2006 Paper
Bib
2005
2002
2001
1994
- Conference and workshop proceedings
2011
- Serge Autexier, Catalin David, Dominik Dietrich, Michael Kohlhase, and Vyacheslav Zholudev
. Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics , In James H. Davenport, William Farmer, Florian Rabe, and Joseph Urban (Ed) Proceedings of Calculemus/MKM 2011, Nr. 6824 of LNAI, p. 164-179, Springer-Verlag Berlin Heidelberg, July, 2011 Bib
- Serge Autexier, Dominik Dietrich, and Marvin Schiller. Cognitive Tutoring in Mathematics based on Assertion Level Reasoning and Proof Strategies (Extended Abstract), In Pedro Quaresma and Ralph-Johan Back (Ed) THedu'11, CTP Components for Educational Software, Workshop associated to CADE-23, Nr. 2011/001 of CISUC Technical Report, p. 11-15, Wroclaw, Poland, Center for Informatics and Systems, University of Coimbra, Portugal, July, 2011 Bib
2010
- Serge Autexier and Christoph Lüth. Adding Change Impact Analysis to the Formal Verification of C Programs, In Dominique Méry and Stephan Merz (Ed) Proceedings 8th International Conference on integrated Formal Methods (IFM2010), LNCS, Nancy, France, Springer, October, 2010 (local copy)
Bib
- Serge Autexier and Normen Müller. Semantics-Based Change Impact Analysis for Heterogeneous Collections of Documents, In Michael Gormish and Rolf Ingold (Ed) Proceedings of 10th ACM Symposium on Document Engineering (DocEng2010), Manchester, UK, September, 2010 (local copy)
Bib
- Serge Autexier and Dominik Dietrich. A Tactic Language for Declarative Proofs, In Matt Kaufmann and Lawrence C. Paulson (Ed) Proceedings International Conference on Interactive Theorem Proving
, Vol. 6172, LNCS, p. 99-114, Edinburgh, Scotland, Springer, July, 2010 (local copy)
Bib
- Serge Autexier and Dominik Dietrich. Recent developments in Omega's proof search programming language, In Lucas Dixon and James Davenport (Ed) Emerging Trends Papers accepted for PLMMS 2010, Vol. 44:2, p. 52-59, ACM SIGSAM, July, 2010 Paper
(local copy)
Bib
2009
2008
2007
- Christoph Benzmüller, Dominik Dietrich, Marvin Schiller, Serge Autexier. Deep Inference for Automated Proof Tutoring?, In Joachim Hertzberg, Michael Beetz, Roman Englert (Ed) KI 2007: Advances in Artificial Intelligence, LNAI, Springer, September, accepted, forthcoming, 2007 (local copy)
Bib
- Serge Autexier, Armin Fiedler, Thomas Neumann, and Marc Wagner. Supporting User-Defined Notations when Integrating Scientific Text-Editors with Proof Assistance , In Manuel Kauers, Manfred Kerber, Robert Miner, and Wolfgang Windsteiger (Ed) Towards Mechanized Mathematical Assistants, LNAI, Springer, June, 2007 Paper
(local copy)
Bib
- Serge Autexier and Marc Wagner. Status Report on the Tight Integration of a Scientific Text-Editor and a Proof Assistance System, In Proceedings of the Workshop on Proof Assistants and Types in Education (PATE'07), Paris, France, June, 2007 (local copy)
Bib
- Marc Wagner, Serge Autexier, Christoph Benzmüller. PLATO: A Mediator between Text-Editors and Proof Assistance Systems, In Serge Autexier, Christoph Benzmüller (Ed) 7th Workshop on User Interfaces for Theorem Provers (UITP'06), Vol. 174(2), Electronic Notes on Theoretical Computer Science, p. 87-107, Elsevier, April, 2007 Paper
(local copy)
Bib
- Serge Autexier, Christoph Benzmüller. Preface, In Serge Autexier, Christoph Benzmüller (Ed) 7th Workshop on User Interfaces for Theorem Provers (UITP'06), Vol. 174(2), Electronic Notes on Theoretical Computer Science, p. 1-2, Elsevier, April, 2007 Paper
Bib
2006
- Serge Autexier and Claudio Sacerdoti-Coen. A Formal Correspondence between OMDoc with Alternative Proofs and the LambdabarMuMutilde-Calculus, In Jon Borwein and Bill Farmer (Ed) Proceedings of MKM'06, Vol. 4108, LNAI, p. 67-81, Springer, August, 2006 Paper
(local copy)
Bib
- Serge Autexier and Dominik Dietrich. Synthesizing Proof Planning Methods and Oants Agents from Mathematical Knowledge, In Jon Borwein and Bill Farmer (Ed) Proceedings of MKM'06, Vol. 4108, LNAI, p. 94-109, Springer, August, 2006 Paper
(local copy)
Bib
- Jürgen Zimmer and Serge Autexier. The MathServe Framework for Semantic Reasoning Web Services, In U. Furbach and N. Shankar (Ed) Proceedings of IJCAR'06, LNAI, p. 140--144, Seattle, USA, Springer, August, 2006 Paper
(local copy)
Bib
- Serge Autexier, Christoph Benzmüller, Armin Fiedler, Henri Lesourd. Integrating Proof Assistants as Reasoning and Verification Tools into a Scientific WYSIWIG Editor, In David Aspinall and Christoph Lüth (Ed) Proceedings of UITP'05, ENTCS, January, 2006 Paper
Bib
- Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, and Claus-Peter Wirth. A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity, In Kohlhase, Michael (Ed) Proceedings of MKM'05, Vol. 3863, LNAI, IUB Bremen, Germany, Springer, January, 2006 Paper
(local copy)
Bib
- Serge Autexier and Armin Fiedler. Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity, In Kohlhase, Michael (Ed) Proceedings of MKM'05, Vol. 3863, LNAI, IUB Bremen, Germany, Springer, January, 2006 Paper
Bib
2005
- Autexier, Serge. On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic, In Beckert, Bernhard (Ed) Proceedings of Tableaux 2005, Vol. 3702, LNAI, Koblenz, Germany, Springer, September, 2005 Paper
(local copy)
Bib
- Autexier, Serge. The CORE Calculus, In Nieuwenhuis, Robert (Ed) Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Vol. 3632, LNAI, Tallinn, Estonia, Springer, July, 2005 Paper
(local copy)
Bib
2004
- Autexier, Serge, Benzmüller, Christoph, Fiedler, Armin, Horacek, Helmut, and Vo, Quoc Bao. Assertion Level Proof Representation with Underspecification, In Kamareddine, Fairouz (Ed) Proceedings of MKM Symposium, Vol. 98, p. 5-23, Heriot-Watt, Edinburgh, February, 2004 Paper
Bib
2003
- Autexier, Serge and Schürmann, Carsten. Disproving False Conjectures, In Vardi, Moshe Y. and Voronkov, Andrei (Ed) Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Vol. 2850, LNAI, p. 33-48, Springer, September, 2003 Paper
(local copy)
Bib
- Hübner, Malte, Benzmüller, Christoph, Autexier, Serge, and Meier, Anreas. Interactive Proof Construction at the Task Level, In Lüth, Christoph and Aspinall, David (Ed) Proceedings of the Workshop User Interfaces for Theorem Provers (UITP'03), Rome, Italy, September, 2003 Bib
- Vo, Bao Quoc, Benzmüller, Christoph, and Autexier, Serge. Assertion Application in Theorem Proving and Proof Planning (Poster description), In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI'03), Acapulco, Mexico, 2003 Bib
2002
- Autexier, Serge and Hutter, Dieter. Maintenance of Formal Software Development by Stratified Verification, In Baaz, Mathias and Voronkov, Andrei (Ed) Proceedings of LPAR'02, LNCS, Tbilissi, Georgia, Springer, September, 2002 Paper
(local copy)
Bib
- Autexier, Serge, Hutter, Dieter, Mossakowski, Till, and Schairer, Axel. The development graph manager MAYA, In Kirchner, Hélène and Ringeissen, Christophe (Ed) Proceedings 9th International Conference on Algebraic Methodology And Software Technology (AMAST'02), Vol. 2422, LNCS, Springer, September, 2002 (local copy)
Bib
- Carsten Schürmann and Serge Autexier. Towards proof planning for Mw+, In Pfenning, Frank (Ed) Proceedings of the Third International Workshop on Logical Frameworks and Meta-Languages (LFM'02), Vol. 70.2, ENTCS, Elsevier Science, July, 2002 Paper
Bib
- Autexier, Serge and Mossakowski, Till. Integrating HOL-CASL into the Development Graph Manager MAYA, In A. Armando (Ed) Proceedings of FROCOS'02, Vol. 2309, LNAI, p. 2-17, Springer, April, 2002 Bib
2001
- Autexier, Serge. A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas, In Bonacina, Maria-Paola and Gramlich, Bernhard (Ed) Proceedings of the 4th Workshop on Strategies in Automated Deduction (STRATEGIES'01), Vol. TR DII 10/01, p. 87-99, Università degli studi di Siena, June, 2001 Bib
- Schairer, Axel, Autexier, Serge, and Hutter, Dieter. A Pragmatic Approach to Reuse in Tactical Theorem Proving, In Bonacina, Maria-Paola and Gramlich, Bernhard (Ed) Proceedings of the 4th Workshop on Strategies in Automated Deduction (STRATEGIES'01), Vol. TR DII 10/01, p. 75-86, Universit\'a degli studi di Siena, June, 2001 Bib
- Mossakowski, Till, Autexier, Serge, and Hutter, Dieter. Extending Development Graphs With Hiding, In Hussmann, Heinrich (Ed) Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), Vol. 2029, LNCS, p. 269-283, Genova, Springer, April, 2001 Bib
2000
1999
- Autexier, Serge, Hutter, Dieter, Mantel, Heiko, and Schairer, Axel. System Description: INKA 5.0 -- A Logic Voyager, In Ganzinger, Harald (Ed) Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Vol. 1632, LNAI, p. 207-211, Trento, Italy, Springer, July, 1999 Bib
1998
- Autexier, S., Mantel, H., and Stephan, W.. Simultaneous Quantifier Elimination, In Herzog, O. and Günter, A (Ed) KI-98: Advances in Artificial Intelligence, 22nd Annual German Conference on Artificial Intelligence, Bremen, Germany, Vol. 1504, LNAI, p. 141-152, Springer, September, 1998 Paper
Bib
1997
- Autexier, Serge and Hutter, Dieter. Equational Proof-Planning by Dynamic Abstraction, In Bonacina, Maria Paola and Furbach, Ulrich (Ed) Proceedings of FTP97: International Workshop First-Order Theorem Proving, Nr. 97-50 of Report Series, p. 1--6, Johannes Kepler Universität, 4040 Linz, Austria, RISC-Linz, October, 1997 Bib
- Theses
2003
1996
- Technical Reports
2009
- Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, and Serge Autexier. Lectures on Jacques Herbrand as a Logician, SEKI Publications, SEKI Report Nr. SR-2009-01 (ISSN 1437-4447), DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str.5, D-28359 Bremen, Germany, 2009 Paper
Bib
2005
2003
1997
- Autexier, Serge. An Abstraction for Proof-Planning: The S-Abstraction, FR 6.2 Informatik, Saarland University, SEKI Report Nr. SR-97-05, Postfach 15 11 50, 66041 Saarbrücken, June, 1997 Bib
- Autexier, Serge and Hutter, Dieter. Parameterized Abstractions used for Proof-Planning, DFKI GmbH, Research Report Nr. RR-97-04, Stuhlsatzenhausweg 3, 66041 Saarbrücken, February, 1997 Bib
1993
- Others
2001
2000