Selected Publications

To appear

Handbook of Automated Reasoning

Chapter on Tableaux and Connections
Reiner Hähnle
To appear in Handbook of Automated Reasoning


Edited by:
J. Alan Robinson and Andrei Voronkov
To appear in 1999, Elsevier Publishers.

Labelled Deduction

Chapter on The SAT Problem of Signed CNF Formulas
Bernhard Beckert, Reiner Hähnle and Felip Manya


Edited by:
Marcello D'Agostino, David Basin, Dov Gabbay, Sean Matthews, Luca Vigano
To appear in 1999, Kluwer Publishing Company.

1999

Handbook of Tableau Methods

Edited by:
Marcello D'Agostino, Dov Gabbay, Reiner Hähnle and Joachim Posegga
670pp. Kluwer Publishing Company.

Handbook of Tableau Methods

Chapter on Tableaux for Multiple-Valued Logics
Reiner Hähnle
pp. 529-580 in Handbook of Tableau Methods, see above.

International Dagstuhl-Seminar 99091 "Deduction"

Semantic Semantic Tableaux
Reiner Hähnle
(Postscript, 108K)

ISMVL 1999

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 (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. (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)

Automated Deduction: a Basis for Applications

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)

Automated Deduction in Multiple-Valued Logics

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
Please send me an e-mail for an order form

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)