Harald Ganzinger

Q: What Schools Are Affiliated With Harald Ganzinger

Harald Ganzinger is affiliated with the following schools: Technical University of Dortmund, Technical University of Munich

Harald Ganzinger's AcademicInfluence.com Rankings

Harald Ganzinger

Computer Science

#2864

World Rank

#2997

Historical Rank

Database

#8254

World Rank

#8616

Historical Rank

computer-science Degrees

Download Badge

Computer Science

Why Is Harald Ganzinger Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Harald Ganzinger was a German computer scientist who together with Leo Bachmair developed the superposition calculus, which is used in most of the state-of-the-art automated theorem provers for first-order logic.

(See a Problem?)

Harald Ganzinger's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

Rewrite-Based Equational Theorem Proving with Selection and Simplification (1994) (496)
Resolution Theorem Proving (2001) (473)
DPLL( T): Fast Decision Procedures (2004) (357)
Attribute coupled grammars (1984) (159)
On Restrictions of Ordered Paramodulation with Simplification (1990) (148)
Automated Deduction — CADE-16 (2002) (140)
New directions in instantiation-based theorem proving (2003) (139)
Basic Paramodulation (1995) (133)
A superposition decision procedure for the guarded fragment with equality (1999) (131)
Set constraints are the monadic class (1993) (129)
Basic Paramodulation and Superposition (1992) (124)
Refutational theorem proving for hierarchic first-order theories (1994) (115)
Equational Reasoning in Saturation-Based Theorem Proving (1998) (100)
A Completion Procedure for Conditional Equations (1988) (100)
The two-variable guarded fragment with transitive relations (1999) (98)
Programs as Data Objects (1986) (94)
Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality (1993) (89)
Smalltalk-80 (1987) (70)
Ordered chaining calculi for first-order theories of transitive relations (1998) (64)
Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability (1983) (63)
A truly generative semantics-directed compiler generator (1982) (62)
Rewrite techniques for transitive relations (1994) (55)
Automated complexity analysis based on ordered resolution (2001) (54)
Integrating Equational Reasoning into Instantiation-Based Theorem Proving (2004) (52)
A New Meta-complexity Theorem for Bottom-Up Logic Programs (2001) (51)
Increasing Modularity and Language-Independency in Automatically Generated Compilers (1983) (51)
Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems (1992) (50)
Logical Algorithms (2002) (49)
A theory of resolution (1997) (47)
Completion-Time Optimization of Rewrite-Time Goal Solving (1989) (47)
Soft Typing for Ordered Resolution (1997) (45)
Complexity analysis based on ordered resolution (1996) (45)
Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems (2001) (44)
Buchberger's Algorithm: A Constraint-Based Completion Procedure (1994) (43)
Theory Instantiation (2006) (41)
Ground Term Confluence in Parametric Conditional Equational Specifications (1987) (40)
Shostak Light (2002) (40)
Perfect Model Semantics for Logic Programs with Equality (1991) (39)
Modular proof systems for partial functions with Evans equality (2006) (39)
Automatic Generation of Optimizing Multipass Compilers (1977) (38)
Superposition with equivalence reasoning and delayed clause normal form transformation (2005) (37)
A Resolution-Based Decision Procedure for Extensions of K4 (1998) (36)
Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract) (1990) (35)
Associative-Commutative Superposition (1994) (35)
Elimination of Equality via Transformation with Ordering Constraints (1998) (33)
Order-Sorted Completion: The Many-Sorted Way (1991) (33)
Ordered Chaining for Total Orderings (1994) (32)
Inductive Theorem Proving by Consistency for First-Order Clauses (1992) (32)
On Storage Optimization for Automatically Generated Compilers (1979) (31)
Chaining techniques for automated theorem proving in many-valued logics (2000) (26)
Rewriting techniques and applications : 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996 : proceedings (1996) (23)
Theorem Proving for Hierarchic First-Order Theories (1992) (22)
Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria (1992) (21)
Operator identification in ADA: formal specification, complexity, and concrete implementation (1980) (20)
Theorem proving in cancellative abelian monoids (1996) (18)
Ordered chaining calculi for first-order theories of binary relations (1995) (17)
Modular Proof Systems for Partial Functions with Weak Equality (2004) (16)
Strict Basic Superposition (1998) (16)
Design evaluation of the compiler generating system MUG1 (1976) (14)
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract) (1996) (14)
Transforming denotational semantics into practical attribute grammars (1980) (14)
Fast Term Indexing with Coded Context Trees (2004) (14)
MUG1 - an incremental compiler-compiler (1976) (14)
Completion with History-Dependent Complexities for Generated Equations (1988) (13)
Denotational Semantics for Languages with Modules (1982) (13)
Context Trees (2001) (13)
Proceedings of the 16th International Conference on Automated Deduction (CADE-16) (1999) (12)
Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings (1994) (12)
Superposition Modulo a Shostak Theory (2003) (12)
Order-Sorted Completion: The Many-Sorted Way (Extended Abstract) (1989) (11)
Programs as Transformations of Algebraic Theories (Extended Abstract) (1981) (11)
Rigid Reachability (1998) (11)
A note on termination in combinatiosn of heterogeneous term rewriting systems (1987) (10)
Decidable Fragments of Simultaneous Rigid Reachability (1999) (9)
System support for modular order-sorted Horn clause specifications (1990) (8)
Logic for Programming and Automated Reasoning (1999) (7)
Strict basic superposition and chaining (1997) (7)
Constraints and Theorem Proving (2001) (7)
Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification (2000) (6)
Modular Logic Programming of Compilers (1985) (5)
Saturation-Based Theorem Proving (Abstract) (1996) (5)
Modular Compiler Descriptions based on Abstract Semantic Data Types (1983) (4)
Modular first-order specifications of operational semantics (1985) (4)
CEC: A System for the Completion of Conditional Equational Specifications (1988) (4)
Automated Deduction - CADE-16: 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings (1999) (4)
Proceedings of the Second European Symposium on Programming (1988) (4)
Programs as Data Objects: Proceedings of a Workshop, Copenhagen, Denmark, October 17 - 19, 1985 (1985) (3)
Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi (2002) (2)
ESOP '88 : 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988 : proceedings (1988) (2)
Rewriting Techniques and Applications (1996) (2)
Knuth-Bendix Completion for Parametric Specifications with Conditional Equations (1986) (2)
An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept (1979) (2)
Formal correctness of Result Checking for Priority Queues (2005) (1)
A Framework for Circular Assume-Guarantee Rules (2002) (1)
CEC (Conditional Equations Completion) (1987) (1)
Proceedings of the 7th International Conference on Rewriting Techniques and Applications (1996) (1)
Description of Parameterized Compiler Modules (1981) (1)
A Systems for the Completion of Conditional Equational Specifications (1988) (0)
Is Logic Effective for Analyzing C Programs (2002) (0)
Strict Basic Superposition and Chaining Authors' Addresses Publication Notes (1997) (0)
Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings (1999) (0)
Constraints and Theorem ProvingLecture Notes for the International Summer School onConstraints in Computational Logics ? (2007) (0)
Max-planck-institut F Ur Informatik Ordered Chaining Calculi for First-order Theories of Binary Relations K I N F O R M a T I K Authors' Addresses Publication Notes (2007) (0)
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract) (1996) (0)
On the design of data abstraction mechanisms for compiler description languages1) (1983) (0)
Foam: A two‐level approach to text formatting on a microcomputer system (1985) (0)
Max-planck-institut F Ur Informatik Associative-commutative Superposition K I N F O R M a T I K (2007) (0)
De idable fragments ofsimultaneous rigid rea hability ? (1999) (0)
Max-planck-institut F Ur Informatik Theorem Proving in Cancellative Abelian Monoids Publication Notes (1996) (0)
Recursive resolution for modal logic (2002) (0)
SIGPLAN(Paper Session) (1976) (0)
Report on the Dagstuhl-Seminar Theorem Proving and Logic Programming with Constraints Organizers : (2012) (0)
Efficient deductive methods for program analysis (2001) (0)
Efficient Implementation of the Graphical Input/Output for Smalltalk-80 (1986) (0)
Bottom-Up Deduction with Deletion and Priorities (2001) (0)
Max-planck-institut F Ur Informatik Rewrite Techniques for Transitive Relations K I N F O R M a T I K (1994) (0)
Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction (1999) (0)
Program Development: Completion Subsystem (1993) (0)
A tribute to referees (2004) (0)
Basic Paramodulation List of Symbols (1995) (0)

This paper list is powered by the following services:

Other Resources About Harald Ganzinger

en.wikipedia.org

What Schools Are Affiliated With Harald Ganzinger?

Harald Ganzinger is affiliated with the following schools: