Harald Ganzinger

104 papers A* 14A 19B 7Journal 19Unranked 39

Year	Rank	Type	Title / Venue / Authors
2006	J	`jnl`	Modular proof systems for partial functions with Evans equality. Inf. Comput. Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann
2006	B	`conf`	Theory Instantiation. LPAR Harald Ganzinger, Konstantin Korovin
2005	J	`jnl`	Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput. Harald Ganzinger, Jürgen Stuber
2004	A*	`conf`	DPLL( T): Fast Decision Procedures. CAV Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2004	J	`jnl`	Fast Term Indexing with Coded Context Trees. J. Autom. Reason. Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
2004	B	`conf`	Integrating Equational Reasoning into Instantiation-Based Theorem Proving. CSL Harald Ganzinger, Konstantin Korovin
2004	A	`conf`	Modular Proof Systems for Partial Functions with Weak Equality. IJCAR Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann
2003	A*	`conf`	New Directions in Instantiation-Based Theorem Proving. LICS Harald Ganzinger, Konstantin Korovin
2003	A	`conf`	Superposition Modulo a Shostak Theory. CADE Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann
2003	A	`conf`	Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. CADE Harald Ganzinger, Jürgen Stuber
2002	B	`conf`	Logical Algorithms. ICLP Harald Ganzinger, David A. McAllester
2002	A	`conf`	Shostak Light. CADE Harald Ganzinger
2001	A	`conf`	A New Meta-complexity Theorem for Bottom-Up Logic Programs. IJCAR Harald Ganzinger, David A. McAllester
2001	J	`jnl`	Automated complexity analysis based on ordered resolution. J. ACM David A. Basin, Harald Ganzinger
2001	—	`conf`	Bottom-Up Deduction with Deletion and Priorities. PADO Harald Ganzinger
2001	A	`conf`	Context Trees. IJCAR Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
2001	A*	`conf`	Efficient deductive methods for program analysis. POPL Harald Ganzinger
2001	A*	`conf`	Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. LICS Harald Ganzinger
2001	—	`ch.`	Resolution Theorem Proving. Handbook of Automated Reasoning Leo Bachmair, Harald Ganzinger
2000	—	`conf`	Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. ISMVL Harald Ganzinger, Viorica Sofronie-Stokkermans
2000	J	`jnl`	Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification. Int. J. Found. Comput. Sci. Harald Ganzinger, Florent Jacquemard, Margus Veanes
1999	A*	`conf`	A Superposition Decision Procedure for the Guarded Fragment with Equality. LICS Harald Ganzinger, Hans de Nivelle
1999	A	`ed.`	Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings CADE Harald Ganzinger
1999	—	`conf`	Constraints and Theorem Proving. CCL Harald Ganzinger, Robert Nieuwenhuis
1999	A*	`conf`	Decidable Fragments of Simultaneous Rigid Reachability. ICALP Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
1999	B	`ed.`	Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings LPAR Harald Ganzinger, David A. McAllester, Andrei Voronkov
1999	A*	`conf`	The Two-Variable Guarded Fragment with Transitive Relations. LICS Harald Ganzinger, Christoph Meyer, Margus Veanes
1998	B	`conf`	A Resolution-Based Decision Procedure for Extensions of K4. Advances in Modal Logic Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt
1998	A	`conf`	Elimination of Equality via Transformation with Ordering Constraints. CADE Leo Bachmair, Harald Ganzinger, Andrei Voronkov
1998	J	`jnl`	Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM Leo Bachmair, Harald Ganzinger
1998	—	`conf`	Rigid Reachability. ASIAN Harald Ganzinger, Florent Jacquemard, Margus Veanes
1998	A	`conf`	Strict Basic Superposition. CADE Leo Bachmair, Harald Ganzinger
1998	J	`jnl`	Wohin geht die automatische Deduktion? Künstliche Intell. Harald Ganzinger, Jörg H. Siekmann, Peter H. Schmitt
1997	A	`conf`	Soft Typing for Ordered Resolution. CADE Harald Ganzinger, Christoph Meyer, Christoph Weidenbach
1996	A*	`conf`	Complexity Analysis Based on Ordered Resolution. LICS David A. Basin, Harald Ganzinger
1996	—	`ed.`	Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings RTA Harald Ganzinger
1996	A*	`conf`	Saturation-Based Theorem Proving (Abstract). ICALP Harald Ganzinger
1996	A	`conf`	Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). CADE Harald Ganzinger
1996	A	`conf`	Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). CADE Harald Ganzinger, Uwe Waldmann
1995	J	`jnl`	Basic Paramodulation Inf. Comput. Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder
1995	—	`conf`	Redundancy and Saturation. UNIF Harald Ganzinger
1994	—	`conf`	Associative-Commutative Superposition. CTRS Leo Bachmair, Harald Ganzinger
1994	—	`conf`	Buchberger's Algorithm: A Constraint-Based Completion Procedure. CCL Leo Bachmair, Harald Ganzinger
1994	—	`conf`	Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings. COMPASS/ADT Leo Bachmair, Harald Ganzinger, Jürgen Stuber
1994	A	`conf`	Ordered Chaining for Total Orderings. CADE Leo Bachmair, Harald Ganzinger
1994	J	`jnl`	Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1994	A*	`conf`	Rewrite Techniques for Transitive Relations LICS Leo Bachmair, Harald Ganzinger
1994	J	`jnl`	Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. Leo Bachmair, Harald Ganzinger
1993	—	`conf`	Program Development: Completion Subsystem. PROSPECTRA Book Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas
1993	A*	`conf`	Set Constraints are the Monadic Class LICS Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1993	—	`conf`	Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. Kurt Gödel Colloquium Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1992	A	`conf`	Basic Paramodulation and Superposition. CADE Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder
1992	—	`ch.`	Inductive Theorem Proving by Consistency for First-Order Clauses. Informatik Harald Ganzinger, Jürgen Stuber
1992	—	`conf`	Inductive Theorem Proving by Consistency for First-Order Clauses. CTRS Harald Ganzinger, Jürgen Stuber
1992	—	`book`	Informatik, Festschrift zum 60. Geburtstag von Günter Hotz Informatik Johannes Buchmann, Harald Ganzinger, Wolfgang J. Paul
1992	J	`jnl`	Konferenzbericht LICS '92. Künstliche Intell. Harald Ganzinger
1992	B	`conf`	Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. LPAR Leo Bachmair, Harald Ganzinger
1992	—	`conf`	Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems. CTRS Harald Ganzinger, Uwe Waldmann
1992	—	`conf`	Theorem Proving for Hierarchic First-Order Theories. ALP Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1991	J	`jnl`	A Completion Procedure for Conditional Equations. J. Symb. Comput. Harald Ganzinger
1991	J	`jnl`	Order-Sorted Completion: The Many-Sorted Way. Theor. Comput. Sci. Harald Ganzinger
1991	B	`conf`	Perfect Model Semantics for Logic Programs with Equality. ICLP Leo Bachmair, Harald Ganzinger
1990	—	`conf`	Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). CTRS Leo Bachmair, Harald Ganzinger
1990	A	`conf`	On Restrictions of Ordered Paramodulation with Simplification. CADE Leo Bachmair, Harald Ganzinger
1990	A*	`conf`	System Support for Modular Order-Sorted Horn Clause Specifications. ICSE Harald Ganzinger, Renate Schäfers
1989	—	`conf`	Completion-Time Optimization of Rewrite-Time Goal Solving. RTA Hubert Bertling, Harald Ganzinger
1989	—	`conf`	Order-Sorted Completion: The Many-Sorted Way (Extended Abstract). TAPSOFT, Vol.1 Harald Ganzinger
1988	A	`conf`	CEC: A System for the Completion of Conditional Equational Specifications. ESOP Hubert Bertling, Harald Ganzinger, Renate Schäfers
1988	A	`ed.`	ESOP '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings ESOP Harald Ganzinger
1987	—	`conf`	A Completion Procedure for Conditional Equations. CTRS Harald Ganzinger
1987	—	`conf`	A Systems for the Completion of Conditional Equational Specifications. CTRS Hubert Bertling, Harald Ganzinger, Renate Schäfers
1987	J	`jnl`	A note on termination in combinatiosn of heterogeneous term rewriting systems. Bull. EATCS Harald Ganzinger, Robert Giegerich
1987	A	`conf`	CEC (Conditional Equations Completion). STACS Hubert Bertling, Harald Ganzinger, Hubert Baumeister
1987	—	`conf`	Completion with History-Dependent Complexities for Generated Equations. ADT Harald Ganzinger
1987	A	`conf`	Ground Term Confluence in Parametric Conditional Equational Specifications. STACS Harald Ganzinger
1987	J	`jnl`	Smalltalk-80. it Inf. Technol. Hubert Baumeister, Harald Ganzinger, Georg Heeg, Michael Rüger
1986	—	`conf`	Efficient Implementation of the Graphical Input/Output for Smalltalk-80. GI Jahrestagung (1) Harald Ganzinger, Georg Heeg
1986	—	`conf`	Knuth-Bendix Completion for Parametric Specifications with Conditional Equations. ADT Harald Ganzinger
1986	—	`conf`	Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung). GI Jahrestagung (1) Harald Ganzinger
1986	—	`ed.`	Programs as Data Objects, Proceedings of a Workshop, Copenhagen, Denmark, October 17-19, 1985 Programs as Data Objects Harald Ganzinger, Neil D. Jones
1985	J	`jnl`	FOAM: A Two-Level Approach to Text Formatting on a Microcomputer System. Softw. Pract. Exp. Harald Ganzinger, Walter Willmertinger
1985	—	`conf`	Modular Logic Programming of Compilers. SLP Harald Ganzinger, Michael Hanus
1985	—	`conf`	Modular first-order specifications of operational semantics. Programs as Data Objects Harald Ganzinger
1984	—	`conf`	Attribute coupled grammars. SIGPLAN Symposium on Compiler Construction Harald Ganzinger, Robert Giegerich
1983	J	`jnl`	Increasing Modularity and Language-Independency in Automatically Generated Compilers. Sci. Comput. Program. Harald Ganzinger
1983	A*	`conf`	Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract). ICALP Harald Ganzinger
1983	—	`conf`	Modular Compiler Descriptions based on Abstract Semantic Data Types. ADT Harald Ganzinger
1983	J	`jnl`	Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability. ACM Trans. Program. Lang. Syst. Harald Ganzinger
1982	—	`conf`	A Truly Generative Semantics-Directed Compiler Generator. SIGPLAN Symposium on Compiler Construction Harald Ganzinger, Robert Giegerich, Ulrich Möncke, Reinhard Wilhelm
1982	—	`conf`	Denotational Semantics for Languages with Modules. Formal Description of Programming Concepts Harald Ganzinger
1982	—	`conf`	Parameterized Specifications - Parameterized Passing and Implementation with Respect to Observability. ADT Harald Ganzinger
1981	—	`conf`	Description of Parameterized Compiler Modules. GI Jahrestagung Harald Ganzinger
1981	—	`conf`	Programs as Transformations of Algebraic Theories (Extended Abstract). GI Jahrestagung Harald Ganzinger
1980	J	`jnl`	Operator identification in ADA: formal specification, complexity, and concrete implementation. ACM SIGPLAN Notices Harald Ganzinger, Knut Ripken
1980	—	`conf`	Transforming denotational semantics into practical attribute grammars. Semantics-Directed Compiler Generation Harald Ganzinger
1979	—	`conf`	An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept. GI Jahrestagung Harald Ganzinger
1979	—	`conf`	On Storage Optimization for Automatically Generated Compilers. Theoretical Computer Science Harald Ganzinger
1978	—	`—`	Optimierende Erzeugung von Übersetzerteilen aus implementierungsorientierten Sprachbeschreibungen. Harald Ganzinger
1977	—	`conf`	Automatic Generation of Optimizing Multipass Compilers. IFIP Congress Harald Ganzinger, Knut Ripken, Reinhard Wilhelm
1976	—	`conf`	Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von Gruppen. Fachtagung über Programmiersprachen Harald Ganzinger
1976	A*	`conf`	Design Evaluation of the Compiler Generating System MUGI. ICSE Reinhard Wilhelm, Knut Ripken, Joachim Ciesinger, Harald Ganzinger, Walter Lahner, R. Nollmann
1976	—	`conf`	MUG1 - an incremental compiler-compiler. ACM Annual Conference Harald Ganzinger, Knut Ripken, Reinhard Wilhelm
1976	—	`conf`	SIGPLAN(Paper Session). ACM Annual Conference Ralph E. Griswold, Harald Ganzinger, Bill P. Buckles, G. C. Hintze, Ken De Jong
1975	—	`conf`	Verschränkung von Compiler-Moduln. GI Jahrestagung Harald Ganzinger, Reinhard Wilhelm