Harald Ganzinger - researchr alias

researchr

You are not signed in
Sign in
Sign up

2006

Modular proof systems for partial functions with Evans equalityHarald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann. iandc, 204(10):1453-1492, 2006. [doi]

Theory InstantiationHarald Ganzinger, Konstantin Korovin. lpar 2006: 497-511 [doi]

2005

Superposition with equivalence reasoning and delayed clause normal form transformationHarald Ganzinger, Jürgen Stuber. iandc, 199(1-2):3-23, 2005. [doi]

2004

2003

Superposition Modulo a Shostak TheoryHarald Ganzinger, Thomas Hillenbrand, Uwe Waldmann. cade 2003: 182-196 [doi]

Superposition with Equivalence Reasoning and Delayed Clause Normal Form TransformationHarald Ganzinger, Jürgen Stuber. cade 2003: 335-349 [doi]

New Directions in Instantiation-Based Theorem ProvingHarald Ganzinger, Konstantin Korovin. lics 2003: 55-64 [doi]

2002

Logical AlgorithmsHarald Ganzinger, David A. McAllester. ICLP 2002: 209-223 [doi]

Shostak LightHarald Ganzinger. cade 2002: 332-346 [doi]

2001

Resolution Theorem ProvingLeo Bachmair, Harald Ganzinger. In John Alan Robinson, Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes). pages 19-99, Elsevier and MIT Press, 2001.

Automated complexity analysis based on ordered resolutionDavid A. Basin, Harald Ganzinger. JACM, 48(1):70-109, 2001. [doi]

Bottom-Up Deduction with Deletion and PrioritiesHarald Ganzinger. pado 2001: 276-278 [doi]

Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word ProblemsHarald Ganzinger. lics 2001: 81-92

Context TreesHarald Ganzinger, Robert Nieuwenhuis, Pilar Nivela. cade 2001: 242-256 [doi]

A New Meta-complexity Theorem for Bottom-Up Logic ProgramsHarald Ganzinger, David A. McAllester. cade 2001: 514-528 [doi]

Efficient deductive methods for program analysisHarald Ganzinger. POPL 2001: 102-103 [doi]

2000

Chaining Techniques for Automated Theorem Proving in Many-Valued LogicsHarald Ganzinger, Viorica Sofronie-Stokkermans. ismvl 2000: 337-344 [doi]

Rigid Reachability, The Non-Symmetric Form of Rigid E-UnificationHarald Ganzinger, Florent Jacquemard, Margus Veanes. ijfcs, 11(1):3-27, 2000.

1999

Decidable Fragments of Simultaneous Rigid ReachabilityVéronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes. icalp 1999: 250-260 [doi]

Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, ProceedingsHarald Ganzinger, editor, Volume 1632 of Lecture Notes in Computer Science, Springer, 1999.

The Two-Variable Guarded Fragment with Transitive RelationsHarald Ganzinger, Christoph Meyer, Margus Veanes. lics 1999: 24-34 [doi]

A Superposition Decision Procedure for the Guarded Fragment with EqualityHarald Ganzinger, Hans de Nivelle. lics 1999: 295-304 [doi]

Logic Programming and Automated Reasoning, 6th International Conference, LPAR 99, Tbilisi, Georgia, September 6-10, 1999, ProceedingsHarald Ganzinger, David A. McAllester, Andrei Voronkov, editors, Volume 1705 of Lecture Notes in Computer Science, Springer, 1999.

Constraints and Theorem ProvingHarald Ganzinger, Robert Nieuwenhuis. iccl 2001: 159-201 [doi]

1998

1997

Soft Typing for Ordered ResolutionHarald Ganzinger, Christoph Meyer, Christoph Weidenbach. cade 1997: 321-335

1996

Complexity Analysis Based on Ordered ResolutionDavid A. Basin, Harald Ganzinger. lics 1996: 456-465

Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)Harald Ganzinger, Uwe Waldmann. cade 1996: 388-402

Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, ProceedingsHarald Ganzinger, editor, Volume 1103 of Lecture Notes in Computer Science, Springer, 1996.

Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract)Harald Ganzinger. cade 1996: 1

Saturation-Based Theorem Proving (Abstract)Harald Ganzinger. icalp 1996: 1-3

1995

Basic ParamodulationLeo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder. iandc, 121(2):172-192, September 1995.

1994

1993

Superposition with Simplification as a Desision Procedure for the Monadic Class with EqualityLeo Bachmair, Harald Ganzinger, Uwe Waldmann. kgc 1993: 83-96

Set Constraints are the Monadic ClassLeo Bachmair, Harald Ganzinger, Uwe Waldmann. lics 1993: 75-83

Program Development: Completion SubsystemHubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas. prospectra 1993: 460-494

1992

1991

Perfect Model Semantics for Logic Programs with EqualityLeo Bachmair, Harald Ganzinger. ICLP 1991: 645-659

Order-Sorted Completion: The Many-Sorted WayHarald Ganzinger. TCS, 89(1):3-32, 1991.

A Completion Procedure for Conditional EquationsHarald Ganzinger. JSC, 11(1/2):51-81, 1991.

1990

Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract)Leo Bachmair, Harald Ganzinger. ctrs 1991: 162-180

On Restrictions of Ordered Paramodulation with SimplificationLeo Bachmair, Harald Ganzinger. cade 1990: 427-441

System Support for Modular Order-Sorted Horn Clause SpecificationsHarald Ganzinger, Renate Schäfers. ICSE 1990: 150-159

1989

Completion-Time Optimization of Rewrite-Time Goal SolvingHubert Bertling, Harald Ganzinger. RTA 1989: 45-58

Order-Sorted Completion: The Many-Sorted Way (Extended Abstract)Harald Ganzinger. tapsoft 1989: 244-258

1988

CEC: A System for the Completion of Conditional Equational SpecificationsHubert Bertling, Harald Ganzinger, Renate Schäfers. ESOP 1988: 378-379

ESOP 88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, ProceedingsHarald Ganzinger, editor, Volume 300 of Lecture Notes in Computer Science, Springer, 1988.

1987

1986

Efficient Implementation of the Graphical Input/Output for Smalltalk-80Harald Ganzinger, Georg Heeg. gi 1986: 151-164

Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung)Harald Ganzinger. gi 1986: 35

Knuth-Bendix Completion for Parametric Specifications with Conditional EquationsHarald Ganzinger. adt 1986:

Programs as Data Objects, Proceedings of a Workshop, Copenhagen, Denmark, October 17-19, 1985Harald Ganzinger, Neil D. Jones, editors, Volume 217 of Lecture Notes in Computer Science, Springer, 1986.

1985

Modular first-order specifications of operational semanticsHarald Ganzinger. pdo 1986: 82-95

Modular Logic Programming of CompilersHarald Ganzinger, Michael Hanus. slp 1985: 242-253

FOAM: A Two-Level Approach to Text Formatting on a Microcomputer SystemHarald Ganzinger, Walter Willmertinger. SPE, 15(4):327-341, 1985.

Programs as Data Objects: PADO 1985Neil D. Jones, Harald Ganzinger, editors, Volume 217 of LNCS, S-V, Copenhagen, Denmark, October 1985.

1984

Attribute coupled grammarsHarald Ganzinger, Robert Giegerich. sigplan 1984: 157-170 [doi]

1983

Parameterized Specifications: Parameter Passing and Implementation with Respect to ObservabilityHarald Ganzinger. TOPLAS, 5(3):318-354, 1983. [doi]

Increasing Modularity and Language-Independency in Automatically Generated CompilersHarald Ganzinger. SCP, 3(3):223-278, 1983.

Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract)Harald Ganzinger. icalp 1983: 237-249

Modular Compiler Descriptions based on Abstract Semantic Data TypesHarald Ganzinger. adt 1983:

1982

Parameterized Specifications - Parameterized Passing and Implementation with Respect to ObservabilityHarald Ganzinger. adt 1982:

A Truly Generative Semantics-Directed Compiler GeneratorHarald Ganzinger, Robert Giegerich, Ulrich Möncke, Reinhard Wilhelm. sigplan 1982: 172-184 [doi]

1981

Programs as Transformations of Algebraic Theories (Extended Abstract)Harald Ganzinger. gi 1981: 32-40

Description of Parameterized Compiler ModulesHarald Ganzinger. gi 1981: 11-19

1980

Transforming denotational semantics into practical attribute grammarsHarald Ganzinger. CC 1980: 1-69

1979

On Storage Optimization for Automatically Generated CompilersHarald Ganzinger. tcs 1979: 132-141

An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics ConceptHarald Ganzinger. gi 1979: 206-217

1976

Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von GruppenHarald Ganzinger. programmier 1976: 194-202

Design Evaluation of the Compiler Generating System MUGIReinhard Wilhelm, Knut Ripken, Joachim Ciesinger, Harald Ganzinger, Walter Lahner, R. Nollmann. ICSE 1976: 571-576

1975

Verschränkung von Compiler-ModulnHarald Ganzinger, Reinhard Wilhelm. gi 1975: 654-665