Harald Ganzinger
Encyclopedia
Harald Ganzinger was a German
computer scientist
that together with Leo Bachmair developed the superposition calculus
, which is (as of 2007) used in most of the state-of-the-art automated theorem provers for first-order logic
.
He received his Ph.D.
from the Technical University of Munich
in 1978. Before 1991 he was a Professor of Computer Science at University of Dortmund. Then he joined the Max Planck Institute for Computer Science
in Saarbrücken
shortly after it was founded in 1991. Until 2004 he was the Director of the Programming Logics department of the Max Planck Institute for Computer Science
and honorary professor at Saarland University
. His research group created the SPASS
automated theorem prover.
He received the Herbrand Award
in 2004 (posthumous) for his important contributions to automated theorem proving
.
Germany
Germany , officially the Federal Republic of Germany , is a federal parliamentary republic in Europe. The country consists of 16 states while the capital and largest city is Berlin. Germany covers an area of 357,021 km2 and has a largely temperate seasonal climate...
computer scientist
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
that together with Leo Bachmair developed the superposition calculus
Superposition calculus
The superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth-Bendix completion...
, which is (as of 2007) used in most of the state-of-the-art automated theorem provers for first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
.
He received his Ph.D.
Doctor of Philosophy
Doctor of Philosophy, abbreviated as Ph.D., PhD, D.Phil., or DPhil , in English-speaking countries, is a postgraduate academic degree awarded by universities...
from the Technical University of Munich
Technical University of Munich
The Technische Universität München is a research university with campuses in Munich, Garching, and Weihenstephan...
in 1978. Before 1991 he was a Professor of Computer Science at University of Dortmund. Then he joined the Max Planck Institute for Computer Science
Max Planck Institute for Computer Science
The Max Planck Institute for Computer Science is devoted to cutting-edge research in computer science with a focus on algorithms and their applications in a broad sense...
in Saarbrücken
Saarbrücken
Saarbrücken is the capital of the state of Saarland in Germany. The city is situated at the heart of a metropolitan area that borders on the west on Dillingen and to the north-east on Neunkirchen, where most of the people of the Saarland live....
shortly after it was founded in 1991. Until 2004 he was the Director of the Programming Logics department of the Max Planck Institute for Computer Science
Max Planck Institute for Computer Science
The Max Planck Institute for Computer Science is devoted to cutting-edge research in computer science with a focus on algorithms and their applications in a broad sense...
and honorary professor at Saarland University
Saarland University
Saarland University is a university located in Saarbrücken, the capital of the German state of Saarland, and Homburg. It was founded in 1948 in Homburg in co-operation with France and is organized in 8 faculties that cover all major fields of science...
. His research group created the SPASS
SPASS theorem prover
SPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus....
automated theorem prover.
He received the Herbrand Award
Herbrand Award
The Herbrand Award for Distinguished Contributions to Automated Deduction is an award given by CADE Inc. to honour persons or groups for important contributions to the field of automated deduction. The award is named after the French scientist Jacques Herbrand and given at most once per CADE or...
in 2004 (posthumous) for his important contributions to automated theorem proving
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
.