| 2006 |
|---|
| 95 | EE | Harald Ganzinger,
Konstantin Korovin:
Theory Instantiation.
LPAR 2006: 497-511 |
| 94 | EE | Harald Ganzinger,
Viorica Sofronie-Stokkermans,
Uwe Waldmann:
Modular proof systems for partial functions with Evans equality.
Inf. Comput. 204(10): 1453-1492 (2006) |
| 2005 |
|---|
| 93 | EE | Harald Ganzinger,
Jürgen Stuber:
Superposition with equivalence reasoning and delayed clause normal form transformation.
Inf. Comput. 199(1-2): 3-23 (2005) |
| 2004 |
|---|
| 92 | EE | Harald Ganzinger,
George Hagen,
Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
DPLL( T): Fast Decision Procedures.
CAV 2004: 175-188 |
| 91 | EE | Harald Ganzinger,
Konstantin Korovin:
Integrating Equational Reasoning into Instantiation-Based Theorem Proving.
CSL 2004: 71-84 |
| 90 | EE | Harald Ganzinger,
Viorica Sofronie-Stokkermans,
Uwe Waldmann:
Modular Proof Systems for Partial Functions with Weak Equality.
IJCAR 2004: 168-182 |
| 89 | EE | Harald Ganzinger,
Robert Nieuwenhuis,
Pilar Nivela:
Fast Term Indexing with Coded Context Trees.
J. Autom. Reasoning 32(2): 103-120 (2004) |
| 2003 |
|---|
| 88 | EE | Harald Ganzinger,
Thomas Hillenbrand,
Uwe Waldmann:
Superposition Modulo a Shostak Theory.
CADE 2003: 182-196 |
| 87 | EE | Harald Ganzinger,
Jürgen Stuber:
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation.
CADE 2003: 335-349 |
| 86 | EE | Harald Ganzinger,
Konstantin Korovin:
New Directions in Instantiation-Based Theorem Proving.
LICS 2003: 55-64 |
| 2002 |
|---|
| 85 | EE | Harald Ganzinger:
Shostak Light.
CADE 2002: 332-346 |
| 84 | EE | Harald Ganzinger,
David A. McAllester:
Logical Algorithms.
ICLP 2002: 209-223 |
| 2001 |
|---|
| 83 | EE | Harald Ganzinger,
Robert Nieuwenhuis,
Pilar Nivela:
Context Trees.
IJCAR 2001: 242-256 |
| 82 | EE | Harald Ganzinger,
David A. McAllester:
A New Meta-complexity Theorem for Bottom-Up Logic Programs.
IJCAR 2001: 514-528 |
| 81 | | Harald Ganzinger:
Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems.
LICS 2001: 81-92 |
| 80 | EE | Harald Ganzinger:
Bottom-Up Deduction with Deletion and Priorities.
PADO 2001: 276-278 |
| 79 | EE | Harald Ganzinger:
Efficient deductive methods for program analysis.
POPL 2001: 102-103 |
| 78 | | Leo Bachmair,
Harald Ganzinger:
Resolution Theorem Proving.
Handbook of Automated Reasoning 2001: 19-99 |
| 77 | EE | David A. Basin,
Harald Ganzinger:
Automated complexity analysis based on ordered resolution.
J. ACM 48(1): 70-109 (2001) |
| 2000 |
|---|
| 76 | EE | Harald Ganzinger,
Viorica Sofronie-Stokkermans:
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics.
ISMVL 2000: 337-344 |
| 75 | | Harald Ganzinger,
Florent Jacquemard,
Margus Veanes:
Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification.
Int. J. Found. Comput. Sci. 11(1): 3-27 (2000) |
| 1999 |
|---|
| 74 | | Harald Ganzinger:
Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings
Springer 1999 |
| 73 | | Harald Ganzinger,
David A. McAllester,
Andrei Voronkov:
Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings
Springer 1999 |
| 72 | EE | Harald Ganzinger,
Robert Nieuwenhuis:
Constraints and Theorem Proving.
CCL 1999: 159-201 |
| 71 | EE | Véronique Cortier,
Harald Ganzinger,
Florent Jacquemard,
Margus Veanes:
Decidable Fragments of Simultaneous Rigid Reachability.
ICALP 1999: 250-260 |
| 70 | EE | Harald Ganzinger,
Christoph Meyer,
Margus Veanes:
The Two-Variable Guarded Fragment with Transitive Relations.
LICS 1999: 24-34 |
| 69 | EE | Harald Ganzinger,
Hans de Nivelle:
A Superposition Decision Procedure for the Guarded Fragment with Equality.
LICS 1999: 295-304 |
| 1998 |
|---|
| 68 | EE | Harald Ganzinger,
Florent Jacquemard,
Margus Veanes:
Rigid Reachability.
ASIAN 1998: 4-21 |
| 67 | | Harald Ganzinger,
Ullrich Hustadt,
Christoph Meyer,
Renate A. Schmidt:
A Resolution-Based Decision Procedure for Extensions of K4.
Advances in Modal Logic 1998: 225-246 |
| 66 | EE | Leo Bachmair,
Harald Ganzinger:
Strict Basic Superposition.
CADE 1998: 160-174 |
| 65 | EE | Leo Bachmair,
Harald Ganzinger,
Andrei Voronkov:
Elimination of Equality via Transformation with Ordering Constraints.
CADE 1998: 175-190 |
| 64 | EE | Leo Bachmair,
Harald Ganzinger:
Ordered Chaining Calculi for First-Order Theories of Transitive Relations.
J. ACM 45(6): 1007-1049 (1998) |
| 63 | | Harald Ganzinger,
Jörg H. Siekmann,
Peter H. Schmitt:
Wohin geht die automatische Deduktion?
KI 12(4): 33-37 (1998) |
| 1997 |
|---|
| 62 | | Harald Ganzinger,
Christoph Meyer,
Christoph Weidenbach:
Soft Typing for Ordered Resolution.
CADE 1997: 321-335 |
| 1996 |
|---|
| 61 | | Harald Ganzinger:
Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings
Springer 1996 |
| 60 | | Harald Ganzinger:
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract).
CADE 1996: 1 |
| 59 | | Harald Ganzinger,
Uwe Waldmann:
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract).
CADE 1996: 388-402 |
| 58 | | Harald Ganzinger:
Saturation-Based Theorem Proving (Abstract).
ICALP 1996: 1-3 |
| 57 | | David A. Basin,
Harald Ganzinger:
Complexity Analysis Based on Ordered Resolution.
LICS 1996: 456-465 |
| 1995 |
|---|
| 56 | | Leo Bachmair,
Harald Ganzinger,
Christopher Lynch,
Wayne Snyder:
Basic Paramodulation
Inf. Comput. 121(2): 172-192 (1995) |
| 1994 |
|---|
| 55 | | Leo Bachmair,
Harald Ganzinger:
Ordered Chaining for Total Orderings.
CADE 1994: 435-450 |
| 54 | | Leo Bachmair,
Harald Ganzinger:
Buchberger's Algorithm: A Constraint-Based Completion Procedure.
CCL 1994: 285-301 |
| 53 | | Leo Bachmair,
Harald Ganzinger,
Jürgen Stuber:
Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings.
COMPASS/ADT 1994: 1-29 |
| 52 | | Leo Bachmair,
Harald Ganzinger:
Associative-Commutative Superposition.
CTRS 1994: 1-14 |
| 51 | | Leo Bachmair,
Harald Ganzinger:
Rewrite Techniques for Transitive Relations
LICS 1994: 384-393 |
| 50 | | Leo Bachmair,
Harald Ganzinger,
Uwe Waldmann:
Refutational Theorem Proving for Hierachic First-Order Theories.
Appl. Algebra Eng. Commun. Comput. 5: 193-212 (1994) |
| 49 | | Leo Bachmair,
Harald Ganzinger:
Rewrite-Based Equational Theorem Proving with Selection and Simplification.
J. Log. Comput. 4(3): 217-247 (1994) |
| 1993 |
|---|
| 48 | | Leo Bachmair,
Harald Ganzinger,
Uwe Waldmann:
Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality.
Kurt Gödel Colloquium 1993: 83-96 |
| 47 | | Leo Bachmair,
Harald Ganzinger,
Uwe Waldmann:
Set Constraints are the Monadic Class
LICS 1993: 75-83 |
| 46 | | Hubert Bertling,
Harald Ganzinger,
Renate Schäfers,
Robert Nieuwenhuis,
Fernando Orejas:
Program Development: Completion Subsystem.
PROSPECTRA Book 1993: 460-494 |
| 1992 |
|---|
| 45 | | Leo Bachmair,
Harald Ganzinger,
Uwe Waldmann:
Theorem Proving for Hierarchic First-Order Theories.
ALP 1992: 420-434 |
| 44 | | Leo Bachmair,
Harald Ganzinger,
Christopher Lynch,
Wayne Snyder:
Basic Paramodulation and Superposition.
CADE 1992: 462-476 |
| 43 | | Harald Ganzinger,
Jürgen Stuber:
Inductive Theorem Proving by Consistency for First-Order Clauses.
CTRS 1992: 226-241 |
| 42 | | Harald Ganzinger,
Uwe Waldmann:
Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems.
CTRS 1992: 430-437 |
| 41 | | Leo Bachmair,
Harald Ganzinger:
Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria.
LPAR 1992: 273-284 |
| 40 | | Harald Ganzinger:
Konferenzbericht LICS '92.
KI 6(3): 51 (1992) |
| 1991 |
|---|
| 39 | | Leo Bachmair,
Harald Ganzinger:
Perfect Model Semantics for Logic Programs with Equality.
ICLP 1991: 645-659 |
| 38 | | Harald Ganzinger:
A Completion Procedure for Conditional Equations.
J. Symb. Comput. 11(1/2): 51-81 (1991) |
| 37 | | Harald Ganzinger:
Order-Sorted Completion: The Many-Sorted Way.
Theor. Comput. Sci. 89(1): 3-32 (1991) |
| 1990 |
|---|
| 36 | | Leo Bachmair,
Harald Ganzinger:
On Restrictions of Ordered Paramodulation with Simplification.
CADE 1990: 427-441 |
| 35 | | Leo Bachmair,
Harald Ganzinger:
Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract).
CTRS 1990: 162-180 |
| 34 | | Harald Ganzinger,
Renate Schäfers:
System Support for Modular Order-Sorted Horn Clause Specifications.
ICSE 1990: 150-159 |
| 1989 |
|---|
| 33 | | Hubert Bertling,
Harald Ganzinger:
Completion-Time Optimization of Rewrite-Time Goal Solving.
RTA 1989: 45-58 |
| 32 | | Harald Ganzinger:
Order-Sorted Completion: The Many-Sorted Way (Extended Abstract).
TAPSOFT, Vol.1 1989: 244-258 |
| 1988 |
|---|
| 31 | | Harald Ganzinger:
ESOP '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings
Springer 1988 |
| 30 | | Hubert Bertling,
Harald Ganzinger,
Renate Schäfers:
CEC: A System for the Completion of Conditional Equational Specifications.
ESOP 1988: 378-379 |
| 1987 |
|---|
| 29 | | Harald Ganzinger:
Completion with History-Dependent Complexities for Generated Equations.
ADT 1987: 73-91 |
| 28 | | Hubert Bertling,
Harald Ganzinger,
Renate Schäfers:
A Systems for the Completion of Conditional Equational Specifications.
CTRS 1987: 249-250 |
| 27 | | Harald Ganzinger:
A Completion Procedure for Conditional Equations.
CTRS 1987: 62-83 |
| 26 | | Harald Ganzinger:
Ground Term Confluence in Parametric Conditional Equational Specifications.
STACS 1987: 286-298 |
| 25 | | Hubert Bertling,
Harald Ganzinger,
Hubert Baumeister:
CEC (Conditional Equations Completion).
STACS 1987: 470 |
| 24 | | Harald Ganzinger,
Robert Giegerich:
A note on termination in combinatiosn of heterogeneous term rewriting systems.
Bulletin of the EATCS 31: 22-27 (1987) |
| 1986 |
|---|
| 23 | | Harald Ganzinger,
Neil D. Jones:
Programs as Data Objects, Proceedings of a Workshop, Copenhagen, Denmark, October 17-19, 1985
Springer 1986 |
| 22 | | Harald Ganzinger:
Knuth-Bendix Completion for Parametric Specifications with Conditional Equations.
ADT 1986 |
| 21 | | Harald Ganzinger,
Georg Heeg:
Efficient Implementation of the Graphical Input/Output for Smalltalk-80.
GI Jahrestagung (1) 1986: 151-164 |
| 20 | | Harald Ganzinger:
Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung).
GI Jahrestagung (1) 1986: 35 |
| 1985 |
|---|
| 19 | | Harald Ganzinger:
Modular first-order specifications of operational semantics.
Programs as Data Objects 1985: 82-95 |
| 18 | | Harald Ganzinger,
Michael Hanus:
Modular Logic Programming of Compilers.
SLP 1985: 242-253 |
| 17 | | Harald Ganzinger,
Walter Willmertinger:
FOAM: A Two-Level Approach to Text Formatting on a Microcomputer System.
Softw., Pract. Exper. 15(4): 327-341 (1985) |
| 1984 |
|---|
| 16 | EE | Harald Ganzinger,
Robert Giegerich:
Attribute coupled grammars.
SIGPLAN Symposium on Compiler Construction 1984: 157-170 |
| 1983 |
|---|
| 15 | | Harald Ganzinger:
Modular Compiler Descriptions based on Abstract Semantic Data Types.
ADT 1983 |
| 14 | | Harald Ganzinger:
Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract).
ICALP 1983: 237-249 |
| 13 | EE | Harald Ganzinger:
Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability.
ACM Trans. Program. Lang. Syst. 5(3): 318-354 (1983) |
| 12 | | Harald Ganzinger:
Increasing Modularity and Language-Independency in Automatically Generated Compilers.
Sci. Comput. Program. 3(3): 223-278 (1983) |
| 1982 |
|---|
| 11 | | Harald Ganzinger:
Parameterized Specifications - Parameterized Passing and Implementation with Respect to Observability.
ADT 1982 |
| 10 | EE | Harald Ganzinger,
Robert Giegerich,
Ulrich Möncke,
Reinhard Wilhelm:
A Truly Generative Semantics-Directed Compiler Generator.
SIGPLAN Symposium on Compiler Construction 1982: 172-184 |
| 1981 |
|---|
| 9 | | Harald Ganzinger:
Description of Parameterized Compiler Modules.
GI Jahrestagung 1981: 11-19 |
| 8 | | Harald Ganzinger:
Programs as Transformations of Algebraic Theories (Extended Abstract).
GI Jahrestagung 1981: 32-40 |
| 1980 |
|---|
| 7 | | Harald Ganzinger:
Transforming denotational semantics into practical attribute grammars.
Semantics-Directed Compiler Generation 1980: 1-69 |
| 1979 |
|---|
| 6 | | Harald Ganzinger:
An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept.
GI Jahrestagung 1979: 206-217 |
| 5 | | Harald Ganzinger:
On Storage Optimization for Automatically Generated Compilers.
Theoretical Computer Science 1979: 132-141 |
| 1977 |
|---|
| 4 | | Harald Ganzinger,
Knut Ripken,
Reinhard Wilhelm:
Automatic Generation of Optimizing Multipass Compilers.
IFIP Congress 1977: 535-540 |
| 1976 |
|---|
| 3 | | Harald Ganzinger:
Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von Gruppen.
Fachtagung über Programmiersprachen 1976: 194-202 |
| 2 | | Reinhard Wilhelm,
Knut Ripken,
Joachim Ciesinger,
Harald Ganzinger,
Walter Lahner,
R. Nollmann:
Design Evaluation of the Compiler Generating System MUGI.
ICSE 1976: 571-576 |
| 1975 |
|---|
| 1 | | Harald Ganzinger,
Reinhard Wilhelm:
Verschränkung von Compiler-Moduln.
GI Jahrestagung 1975: 654-665 |
