Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Selected PublicationsBack to Reiner's Home Page
Selected Publications
My personal bibliography containing BiBTeX entries for the following
(and many more) papers is here (750kB, ca. 2000
entries).
To appear
ISMIS 2005
Normal Forms for Knowledge Compilation Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings ISMIS'05, Saratoga Springs/NY, USA
Preprint (PDF) (Final version will appear in LNCS)
2nd International Conference on Security in Pervasive Computing
A Theorem Proving Approach to Analysis of Secure Information Flow Ádám Darvas, Reiner Hähnle, Dave Sands
Boppard, Germany
Preprint (PDF) (Final version will appear in LNCS)
Software Tools for Technology Transfer
Formal Specification of Security-Critical Railway
Software with the KeY System Richard Bubel and Reiner Hähnle
Springer-Verlag
Preprint (PDF), Online First
2005
Software and System Modeling
The KeY Tool Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert,
Richard Bubel, Martin Giese, Reiner Hähnle,
Wolfram Menzel, Wojciech Mostowski, Andreas Roth,
Steffen Schlager, and Peter H. Schmitt
Springer-Verlag, 4(1):32-54, 2005 Springer Online
CASSIS'04
Verification of Safety Properties in the Presence of Transactions Reiner Hähnle and Wojciech Mostowski
Post Conference Proceedings, CASSIS: Construction and
Analysis of Safe, Secure and Interoperable Smart devices,
Marseille
Springer-Verlag, LNCS 3362 pp 151-171, 2005, preprint
(PDF), Springer
Online
Taclets: A New Paradigm for Constructing Interactive Theorem Provers Bernhard Beckert, Martin Giese, Elmar Habermalz,
Reiner Hähnle, Andreas Roth, Philipp Rümmer,
and Steffen Schlager, (PDF)
Volume 98(1), pp 17-54
UML 2004 workshop on OCL and Model Driven Engineering
Rule-Based Simplification of OCL Constraints Martin Giese, Reiner Hähnle, and Daniel Larsson
Workshop Proceedings
(PDF)
2003
FATES 2003
Using a software testing technique to improve theorem
proving Reiner Hähnle and Angela Wallenburg
Post Conference Proceedings,
3rd International Workshop on Formal Approaches
to Testing of Software (FATES), Montréal, Canada
(PDF)
Tableaux 2003
Tableaux and Constraints Martin Giese and Reiner Hähnle
Position papers, Tableaux 2003, Rome, Italy
(gzipped
PS)
Fair Constraint Merging Tableaux in Lazy Functional Programming Style Reiner Hähnle and Niklas Sörensson
System Description, Tableaux 2003, Rome, Italy
(PDF), Extended
Version (PDF), Springer-Verlag LNAI.
Workshop on Formal Methods for Industrial Critical Systems (FMICS 03)
Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System Richard Bubel and Reiner Hähnle
Invited Paper, FMICS 2003, Røros, Norway
(PDF), ENTCS Vol 80
Workshop on Issues in the Theory of Security (WITS'03)
A Theorem Proving Approach to Analysis of Secure Information Flow Ádám Darvas, Reiner Hähnle, Dave Sands
Affiliated to ETAPS 2003, Warsaw, Poland
(PDF)
2002
Journal of the Information Processing Society of Japan
Model Generation Theorem Proving with Finite
Interval Constraints Reiner Hähnle and Ryuzo Hasegawa and Yasuyuki Shirai
Volume 43, number 12.
Chapter on Complexity of Many-Valued Logics Reiner Hähnle
Edited by: Melvin Fitting and Ewa Orlowska
Volume 114 of Studies in Fuzziness and Soft Computing,
Physica Verlag.
Tableaux 2002
Unit Preference for Ordered Resolution
and for Connection Graph Resolution Reiner Hähnle, Neil Murray, Erik Rosenthal
Position papers, Tableaux 2002, Copenhagen, Denmark
(PDF)
Workshop on Problems and Problem Sets (affiliated to
CADE-18), Copenhagen, Denmark
Verification of Hardware Systems with First-Order Logic Koen Claessen, Reiner Hähnle, Johan Mårtensson (pdf, 134K)
FASE 2002
An Authoring Tool for Informal and Formal Requirements Specifications Reiner Hähnle and Kristofer Johannisson and Aarne Ranta
Proceedings Fundamental Approaches to Software Engineering (FASE),
Part of Joint European Conferences on Theory and Practice
of Software, ETAPS, Grenoble.
2002. Springer-Verlag LNAI.
(pdf, 362K)
FASE 2002
The KeY System: Integrating Object-Oriented Design and Formal Methods Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert,
Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski
and Peter H. Schmitt
Proceedings Fundamental Approaches to Software Engineering (FASE),
Part of Joint European Conferences on Theory and Practice
of Software, ETAPS, Grenoble.
2002. Springer-Verlag LNAI.
(pdf, 117K)
Ordered Resolution vs. Connection Graph Resolution Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings International Joint Conference on
Automated Reasoning, Siena, Italy
2001. Springer-Verlag LNAI.
(gzipped Postscript, 83K)
Computational Intelligence in Theory and Practice
Chapter on Proof Theory of Many-Valued
Logic and Linear Optimization Reiner Hähnle
Edited by: Bernd Reusch and Karl-Heinz Temme
Advances in Soft Computing Series, Physica-Verlag, Heidelberg.
ISMVL 2001
A Modular Reduction of Regular Logic to Classical Logic Ramon Bejar, Reiner Hähnle and Felip Manya
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'2001, Warsaw, Poland, IEEE CS Press. (gzipped Postscript, 47K)
ISMVL 2001
Complexity of Many-Valued Logics (Invited Tutorial) Reiner Hähnle
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'2001, Warsaw, Poland, IEEE CS Press. (gzipped Postscript, 83K)
ETAPS 2001 Workshop on Transformations in UML (WTUML),
Genova, Italy
The KeY Approach: Integrating Object Oriented
Design and Formal Verification Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert,
Martin Giese, Elmar Habermalz, Reiner
Hähnle, Wolfram Menzel and Peter H. Schmitt (gzipped
Postscript, 144K)
Java Card Workshop, Cannes
The KeY Approach: Integrating Object Oriented
Design and Formal Verification Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert,
Martin Giese, Elmar Habermalz, Reiner
Hähnle, Wolfram Menzel and Peter H. Schmitt (gzipped
Postscript, 40K)
Softwaretechnik 2000, Berlin
Entwurfsmustergesteuerte Erzeugung von OCL-Constraints Thomas Baar and Reiner Hähnle and Theo Sattler
and Peter H. Schmitt (gzipped
Postscript, 95K)
First International Conference on Computational Logic,
CL 2000, Stream on Logic Programming:
Theory and Extensions, London, UK
Model Generation Theorem Proving with Finite
Interval Constraints Reiner Hähnle and Ryuzo Hasegawa and Yasuyuki Shirai (gzipped
Postscript, 85K)
Chapter on The SAT Problem of Signed CNF Formulas Bernhard Beckert, Reiner Hähnle and Felip Manyà
Edited by: Marcello D'Agostino, David Basin, Dov Gabbay, Séan Matthews, Luca Viganó
Volume 17 of Applied Logic Series, Kluwer.
ISMVL 2000
On the Regular 2-SAT Problem Bernhard Beckert, Reiner Hähnle and Felip Manya
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'2000, Portland/OR, USA, IEEE CS Press.
(gzipped Postscript, 45K)
Transformations between Signed and Classical Clause Logic Bernhard Beckert, Reiner Hähnle and Felip Manya
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'99, Freiburg, Germany
(gzipped Postscript, 61K)
1998
KI - Künstliche Intelligenz
Integrierter Deduktiver Software-Entwurf Reiner Hähnle, Wolfram Menzel, Peter Schmitt
Issue 4/98 (December), pp. 40-41, 1998.
Journal of Logic and Computation
Simplification of Many-Valued Logic Formulas Using
Anti-Links Bernhard Beckert, Reiner Hähnle, Gonzalo Escalada-Imaz
Volume 8(4), pp. 569-588, 1998.
(gzipped Postscript, 79K)
Studia Logica. Special Issue on Many-Valued Logics,
their Proof Theory and Algebras, edited by D. Mundici.
Commodious Axiomatization of Quantifiers in Multiple-Valued Logic Reiner Hähnle
Volume 61(1), pp. 101-121, 1998.
(Postscript, 77K)
Edited by: Wolfgang Bibel and Peter Schmitt
Volume I-III, Kluwer Publishing Company 1998.
Chapter I.1: Analytic Tableaux Bernhard Beckert and Reiner Hähnle
Chapter II.4: Integrating Automated and Interactive Theorem Proving Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel,
Wolfgang Reif, Gerhard Schellhorn, Peter Schmitt
Tableaux 1998
Some Remarks on Completeness, Connection
Graph Resolution and Link Deletion Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings Tableaux 1998, Tilburg, Netherlands
(Postscript, 56K)
1997
Mathware and Soft Computing
Deduction in Many-Valued Logics: a Survey Reiner Hähnle and Gonzalo Escalada-Imaz
Vol. IV, Number 2, pp. 69-97
(Postscript, 91K)
Soft Computing: A Fusion of Foundations, Methodologies and Applications
Proof Theory of Many-Valued
Logic - Linear Optimization - Logic Design:
Connections and Interactions Reiner Hähnle
Vol. 1, Number 3, pp. 107-119
Kurt-Gödel-Colloquium 1997
Restart Tableaux with Selection Function Christian Pape and Reiner Hähnle
Proceedings KGC'97, Vienna, Austria
(Postscript, 82K)
ISMIS 1997
Completeness for Linear Regular Negation
Normal Form Inference Systems Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings ISMIS'97, Charlotte/NC, USA
(Postscript, 61K)
Journal of Automated Reasoning
Fast Subsumption Checks Using Anti-Links Anavai Ramesh and Neil V. Murray and Bernhard Beckert and Reiner Hähnle
Vol. 18, Number 1, pp. 47-84
(Postscript, 109K)
Tableaux 1997
Ordered Tableaux: Extensions and Applications Reiner Hähnle and Christian Pape
Proceedings TABLEAUX'97, Pont-a-Mousson, France
(Postscript, 66K)
1996
Journal of Logic and Computation
A-Ordered Tableaux Reiner Hähnle and Stefan Klingenbeck Vol. 6, Number 6, pp. 819-834
(Postscript, 123K)
CADE-13 1996
The Many-Valued Tableau-Based Theorem Prover 3TAP:
Version 4.0 (System Abstract) Bernhard Beckert, Reiner Hähnle, Peter Oel and Martin Sulzmann
Proc. 13th Conference on Automated Deduction CADE, New Brunswick/NJ, USA,
(Postscript, 30K)
ISMVL 1996
Commodious Axiomatization of Quantifiers in Multiple-Valued Logic Reiner Hähnle
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'96, Santiago de Compostela, Spain
(Postscript, 63K)
Journal of Applied Non-Classical Logics
Exploiting Data Dependencies in Many-Valued Logics Reiner Hähnle Vol. 6, Number 1, pp. 49-69
(Postscript, 68K)
1995
Post ILPS Workshop on Interval Constraints 1995, Portland/OR, USA
Model Generation Theorem Proving with Interval Constraints Reiner Hähnle and Ryuzo Hasegawa and Yasuyuki Shirai (Postscript, 89K)
Computer Science Logic 1995, Paderborn/Germany
Deduction by Combining Semantic Tableaux and Integer Programming Bernhard Beckert and Reiner Hähnle (Postscript, 54K)
Collegium Logicum. Annals of the Kurt-Goedel-Society
Automated Deduction and Integer Programming Reiner Hähnle
Vol. 1, pp. 67-86, Springer-Verlag
Proceedings of: Theorem Proving with Analytic Tableaux
and Related Methods, 4th International Workshop, St. Goar,
Germany
Peter Baumgartner, Reiner Hähnle and Joachim Posegga
LNAI 918, Springer-Verlag
1994
Journal of Automated Reasoning
The liberalized delta-rule in free variable semantic tableaux Reiner Hähnle and Peter H. Schmitt
Vol. 13, Number 2, pp. 211-222
(DVI, 30K)
Annals of Math and AI
Many-Valued Logic and Mixed Integer Programming Reiner Hähnle
Vol. 12, Numbers 3-4, pp. 231-264
(DVI, 53K)
Journal of Logic and Computation
Short Conjunctive Normal Forms in Finitely-Valued Logics Reiner Hähnle
Vol. 4, Number 6, pp. 905-927
(DVI, 76K)
ICTL 1994
Improving Temporal Logic Tableaux Using Integer Constraints Reiner Hähnle and Ortrun Ibens
Proc.~International Conference on Temporal Logic, Bonn, Germany
(postscript, 38K)
Reiner Hähnle
International Series of Monographs on Computer Science 10,
Oxford University
Press
Reviewed in Computing Reviews, August 1995,
pp. 409-410, #9508-0571; Notre Dame Journal Formal Logic, 37(4),
Fall 1996; Mathematical Reviews 1996, #96a:68107
The book is out of print now. You can download a copy for your
personal use from here
(with permission from Oxford University
Press).
CADE-12 1994
Semantic Tableaux with Ordering Restrictions Stefan Klingenbeck and Reiner Hähnle
Proc. 12th Conference on Automated Deduction CADE, Nancy, France,
(postscript, 76K)
LPAR 1994
On Anti-Links Bernhard Beckert, Reiner Hähnle, Neil Murray, Anavai Ramesh
Proc. 5th International Conference on Logic Programming and Automated Reasoning, Kiev, Ukraine
(postscript, 54K)
ISMVL 1994
Efficient Deduction in Many-Valued Logics Reiner Hähnle
Proc. International Symposium on Multiple-Valued Logics, ISMVL'94, Boston/MA, USA
(postscript, 103K)
1993
KGC 1993
The even more liberalized delta-rule in free variable semantic tableaux Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Proceedings of the third Kurt Goedel Colloquium KGC'93, Brno, Czech Republic
(DVI, 25K)
ISMIS 1993
Short Normal Forms for Arbitrary Finitely-Valued Logics Reiner Hähnle
Proceedings ISMIS'93, Trondheim, Norway
(DVI, 32K)
LPAR 1993
Verification of Switch Level Designs with Many-Valued Logic Reiner Hähnle and Werner Kernig
Proc.~{LPAR}'93, St.~Petersburg, Russia
(DVI, 30K)
1992
CADE-11 1992
An Improved Method for Adding Equality to Free Variable Semantic Tableaux Bernhard Beckert and Reiner Hähnle
Proc. 11th Conference on Automated Deduction CADE, Albany/NY, USA,
(DVI, 45K)
CADE-11 1992
The Many-Valued Tableau-Based Theorem Prover 3TAP (System Abstract) Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig
Proc. 11th Conference on Automated Deduction CADE, Albany/NY, USA,
(DVI, 7K)
AISMC-1
A New Translation from Deduction into Integer Programming Reiner Hähnle
Proc. Int. Conf. on Artificial Intelligence and Symbolic Mathematical Computing AISMC-1, Karlsruhe, Germany
(DVI, 34K)
1991
ISMVL 1991
Uniform Notation of Tableaux Rules for Multiple-Valued Logics Reiner Hähnle
Proc. International Symposium on Multiple-Valued Logic, Victoria, Canada,
(DVI, 49K)
1990
CSL 1990
Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics Reiner Hähnle
Proc. Computer Science Logic, Heidelberg, Germany,
(DVI, 39K)