Harald Ganzinger

According to our database, Harald Ganzinger authored at least 96 papers between 1975 and 2006.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2006

Modular proof systems for partial functions with Evans equality.

Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann

Inf. Comput., 2006

Theory Instantiation.

Harald Ganzinger, Konstantin Korovin

Proceedings of the Logic for Programming, 2006

2005

Superposition with equivalence reasoning and delayed clause normal form transformation.

Harald Ganzinger, Jürgen Stuber

Inf. Comput., 2005

2004

Fast Term Indexing with Coded Context Trees.

Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela

J. Autom. Reason., 2004

Integrating Equational Reasoning into Instantiation-Based Theorem Proving.

Harald Ganzinger, Konstantin Korovin

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

DPLL( T): Fast Decision Procedures.

Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Modular Proof Systems for Partial Functions with Weak Equality.

Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

New Directions in Instantiation-Based Theorem Proving.

Harald Ganzinger, Konstantin Korovin

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Superposition Modulo a Shostak Theory.

Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Logical Algorithms.

Harald Ganzinger, David A. McAllester

Proceedings of the Logic Programming, 18th International Conference, 2002

Shostak Light.

Harald Ganzinger

Proceedings of the Automated Deduction, 2002

2001

Automated complexity analysis based on ordered resolution.

David A. Basin, Harald Ganzinger

J. ACM, 2001

Efficient deductive methods for program analysis.

Harald Ganzinger

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

Bottom-Up Deduction with Deletion and Priorities.

Harald Ganzinger

Proceedings of the Programs as Data Objects, Second Symposium, 2001

Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems.

Harald Ganzinger

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

Context Trees.

Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

A New Meta-complexity Theorem for Bottom-Up Logic Programs.

Harald Ganzinger, David A. McAllester

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Resolution Theorem Proving.

Leo Bachmair, Harald Ganzinger

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification.

Harald Ganzinger, Florent Jacquemard, Margus Veanes

Int. J. Found. Comput. Sci., 2000

Chaining Techniques for Automated Theorem Proving in Many-Valued Logics.

Harald Ganzinger, Viorica Sofronie-Stokkermans

Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic, 2000

1999

A Superposition Decision Procedure for the Guarded Fragment with Equality.

Harald Ganzinger, Hans de Nivelle

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

The Two-Variable Guarded Fragment with Transitive Relations.

Harald Ganzinger, Christoph Meyer, Margus Veanes

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Decidable Fragments of Simultaneous Rigid Reachability.

Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes

Proceedings of the Automata, 1999

Constraints and Theorem Proving.

Harald Ganzinger, Robert Nieuwenhuis

Proceedings of the Constraints in Computational Logics: Theory and Applications, 1999

1998

Wohin geht die automatische Deduktion?

Harald Ganzinger, Jörg H. Siekmann, Peter H. Schmitt

Künstliche Intell., 1998

Ordered Chaining Calculi for First-Order Theories of Transitive Relations.

Leo Bachmair, Harald Ganzinger

J. ACM, 1998

Elimination of Equality via Transformation with Ordering Constraints.

Leo Bachmair, Harald Ganzinger, Andrei Voronkov

Proceedings of the Automated Deduction, 1998

Strict Basic Superposition.

Leo Bachmair, Harald Ganzinger

Proceedings of the Automated Deduction, 1998

Rigid Reachability.

Harald Ganzinger, Florent Jacquemard, Margus Veanes

Proceedings of the Advances in Computing Science, 1998

A Resolution-Based Decision Procedure for Extensions of K4.

Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt

Proceedings of the Advances in Modal Logic 2, 1998

1997

Soft Typing for Ordered Resolution.

Harald Ganzinger, Christoph Meyer, Christoph Weidenbach

Proceedings of the Automated Deduction, 1997

1996

Complexity Analysis Based on Ordered Resolution.

David A. Basin, Harald Ganzinger

Proceedings of the Proceedings, 1996

Saturation-Based Theorem Proving (Abstract).

Harald Ganzinger

Proceedings of the Automata, Languages and Programming, 23rd International Colloquium, 1996

Theorem Proving in Cancellative Abelian Monoids (Extended Abstract).

Harald Ganzinger, Uwe Waldmann

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract).

Harald Ganzinger

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

Basic Paramodulation

Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder

Inf. Comput., September, 1995

Redundancy and Saturation.

Harald Ganzinger

Proceedings of the 9th International Workshop on Unification, 1995

1994

Rewrite-Based Equational Theorem Proving with Selection and Simplification.

Leo Bachmair, Harald Ganzinger

J. Log. Comput., 1994

Refutational Theorem Proving for Hierarchic First-Order Theories.

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Appl. Algebra Eng. Commun. Comput., 1994

Rewrite Techniques for Transitive Relations

Leo Bachmair, Harald Ganzinger

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Associative-Commutative Superposition.

Leo Bachmair, Harald Ganzinger

Proceedings of the Conditional and Typed Rewriting Systems, 4th International Workshop, 1994

Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings.

Leo Bachmair, Harald Ganzinger, Jürgen Stuber

Proceedings of the Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30, 1994

Buchberger's Algorithm: A Constraint-Based Completion Procedure.

Leo Bachmair, Harald Ganzinger

Proceedings of the Constraints in Computational Logics, First International Conference, 1994

Ordered Chaining for Total Orderings.

Leo Bachmair, Harald Ganzinger

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

Program Development: Completion Subsystem.

Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas

Proceedings of the Program Development by Specification and Transformation, 1993

Set Constraints are the Monadic Class

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality.

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Proceedings of the Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, 1993

1992

Konferenzbericht LICS '92.

Harald Ganzinger

Künstliche Intell., 1992

Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria.

Leo Bachmair, Harald Ganzinger

Proceedings of the Logic Programming and Automated Reasoning, 1992

Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems.

Harald Ganzinger, Uwe Waldmann

Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Inductive Theorem Proving by Consistency for First-Order Clauses.

Harald Ganzinger, Jürgen Stuber

Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Basic Paramodulation and Superposition.

Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder

Proceedings of the Automated Deduction, 1992

Theorem Proving for Hierarchic First-Order Theories.

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Proceedings of the Algebraic and Logic Programming, 1992

Inductive Theorem Proving by Consistency for First-Order Clauses.

Harald Ganzinger, Jürgen Stuber

Proceedings of the Informatik, Festschrift zum 60. Geburtstag von Günter Hotz, 1992

1991

Order-Sorted Completion: The Many-Sorted Way.

Harald Ganzinger

Theor. Comput. Sci., 1991

A Completion Procedure for Conditional Equations.

Harald Ganzinger

J. Symb. Comput., 1991

Perfect Model Semantics for Logic Programs with Equality.

Leo Bachmair, Harald Ganzinger

Proceedings of the Logic Programming, 1991

1990

System Support for Modular Order-Sorted Horn Clause Specifications.

Harald Ganzinger, Renate Schäfers

Proceedings of the 12th International Conference on Software Engineering, 1990

Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract).

Leo Bachmair, Harald Ganzinger

Proceedings of the Conditional and Typed Rewriting Systems, 1990

On Restrictions of Ordered Paramodulation with Simplification.

Leo Bachmair, Harald Ganzinger

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

Order-Sorted Completion: The Many-Sorted Way (Extended Abstract).

Harald Ganzinger

Proceedings of the TAPSOFT'89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1989

Completion-Time Optimization of Rewrite-Time Goal Solving.

Hubert Bertling, Harald Ganzinger

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

1988

CEC: A System for the Completion of Conditional Equational Specifications.

Hubert Bertling, Harald Ganzinger, Renate Schäfers

Proceedings of the ESOP '88, 1988

1987

Smalltalk-80.

Hubert Baumeister, Harald Ganzinger, Georg Heeg, Michael Rüger

it Inf. Technol., 1987

A note on termination in combinatiosn of heterogeneous term rewriting systems.

Harald Ganzinger, Robert Giegerich

Bull. EATCS, 1987

Ground Term Confluence in Parametric Conditional Equational Specifications.

Harald Ganzinger

Proceedings of the STACS 87, 1987

CEC (Conditional Equations Completion).

Hubert Bertling, Harald Ganzinger, Hubert Baumeister

Proceedings of the STACS 87, 1987

A Systems for the Completion of Conditional Equational Specifications.

Hubert Bertling, Harald Ganzinger, Renate Schäfers

Proceedings of the Conditional Term Rewriting Systems, 1987

Completion with History-Dependent Complexities for Generated Equations.

Harald Ganzinger

Proceedings of the Recent Trends in Data Type Specification, 1987

1986

Efficient Implementation of the Graphical Input/Output for Smalltalk-80.

Harald Ganzinger, Georg Heeg

Proceedings of the GI - 16. Jahrestagung I, Berlin, 6.-10. Oktober 1986, Proceedings, 1986

Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung).

Harald Ganzinger

Proceedings of the GI - 16. Jahrestagung I, Berlin, 6.-10. Oktober 1986, Proceedings, 1986

Knuth-Bendix Completion for Parametric Specifications with Conditional Equations.

Harald Ganzinger

Proceedings of the 4st Workshop on Abstract Data Type, 1986

1985

FOAM: A Two-Level Approach to Text Formatting on a Microcomputer System.

Harald Ganzinger, Walter Willmertinger

Softw. Pract. Exp., 1985

Modular Logic Programming of Compilers.

Harald Ganzinger, Michael Hanus

Proceedings of the 1985 Symposium on Logic Programming, 1985

Modular first-order specifications of operational semantics.

Harald Ganzinger

Proceedings of the Programs as Data Objects, 1985

1984

Attribute coupled grammars.

Harald Ganzinger, Robert Giegerich

Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction, 1984

1983

Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability.

Harald Ganzinger

ACM Trans. Program. Lang. Syst., 1983

Increasing Modularity and Language-Independency in Automatically Generated Compilers.

Harald Ganzinger

Sci. Comput. Program., 1983

Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract).

Harald Ganzinger

Proceedings of the Automata, 1983

Modular Compiler Descriptions based on Abstract Semantic Data Types.

Harald Ganzinger

Proceedings of the Proceedings 2nd Workshop on Abstract Data Type, 1983

1982

A Truly Generative Semantics-Directed Compiler Generator.

Harald Ganzinger, Robert Giegerich, Ulrich Möncke, Reinhard Wilhelm

Proceedings of the SIGPLAN '82 Symposium on Compiler Construction, 1982

Denotational Semantics for Languages with Modules.

Harald Ganzinger

Proceedings of the Formal Description of Programming Concepts : Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts- II, 1982

Parameterized Specifications - Parameterized Passing and Implementation with Respect to Observability.

Harald Ganzinger

Proceedings of the Proceedings 1st Workshop on Abstract Data Type, 1982

1981

Programs as Transformations of Algebraic Theories (Extended Abstract).

Harald Ganzinger

Proceedings of the GI, 1981

Description of Parameterized Compiler Modules.

Harald Ganzinger

Proceedings of the GI, 1981

1980

Operator identification in ADA: formal specification, complexity, and concrete implementation.

Harald Ganzinger, Knut Ripken

ACM SIGPLAN Notices, 1980

Transforming denotational semantics into practical attribute grammars.

Harald Ganzinger

Proceedings of the Semantics-Directed Compiler Generation, 1980

1979

On Storage Optimization for Automatically Generated Compilers.

Harald Ganzinger

Proceedings of the Theoretical Computer Science, 1979

An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept.

Harald Ganzinger

Proceedings of the GI - 9. Jahrestagung, Bonn, 1.-5. Oktober 1979, Proceedings, 1979

1978

Optimierende Erzeugung von Übersetzerteilen aus implementierungsorientierten Sprachbeschreibungen.

Harald Ganzinger

PhD thesis, 1978

1977

Automatic Generation of Optimizing Multipass Compilers.

Harald Ganzinger, Knut Ripken, Reinhard Wilhelm

Proceedings of the Information Processing, 1977

1976

Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von Gruppen.

Harald Ganzinger

Proceedings of the Programmiersprachen, 1976

Design Evaluation of the Compiler Generating System MUGI.

Reinhard Wilhelm, Knut Ripken, Joachim Ciesinger, Harald Ganzinger, Walter Lahner, R. Nollmann

Proceedings of the 2nd International Conference on Software Engineering, 1976

SIGPLAN(Paper Session).

Ralph E. Griswold, Harald Ganzinger, Bill P. Buckles, G. C. Hintze, Ken De Jong

Proceedings of the 1976 Annual Conference, Houston, Texas, USA, October 20-22, 1976, 1976

MUG1 - an incremental compiler-compiler.

Harald Ganzinger, Knut Ripken, Reinhard Wilhelm

Proceedings of the 1976 Annual Conference, Houston, Texas, USA, October 20-22, 1976, 1976

1975

Verschränkung von Compiler-Moduln.

Harald Ganzinger, Reinhard Wilhelm

Proceedings of the GI - 5. Jahrestagung, Dortmund, 8.-10. Oktober 1975, 1975