Travelled to:1 × Australia
1 × Czech Republic
1 × Ireland
1 × Poland
1 × Spain
1 × United Kingdom
10 × USA
2 × Canada
2 × Germany
3 × Denmark
3 × Italy
5 × France
Collaborated with:∅ L.Bachmair U.Waldmann K.Korovin D.A.McAllester R.Schäfers H.Bertling R.Giegerich C.Meyer M.Veanes R.Nieuwenhuis J.Stuber H.d.Nivelle D.A.Basin M.Hanus R.Wilhelm V.Sofronie-Stokkermans T.Hillenbrand P.Nivela A.Voronkov C.Weidenbach V.Cortier F.Jacquemard C.Lynch W.Snyder U.Möncke G.Hagen A.Oliveras C.Tinelli K.Ripken J.Ciesinger W.Lahner R.Nollmann
Talks about:order (9) theorem (7) prove (6) base (6) superposit (5) semant (5) program (4) modular (4) system (4) compil (4)
Person: Harald Ganzinger
DBLP: Ganzinger:Harald
Facilitated 3 volumes:
Ed
Ed
EdContributed to:
2004
2004
20042003
20032002
200220012001
2001
199919991998199719961996199619941994
1992199219911990
1990198919881985
198419831982
19801976
1989Wrote 38 papers:
- CAV-2004-GanzingerHNOT #performance
- DPLL( T): Fast Decision Procedures (HG, GH, RN, AO, CT), pp. 175–188.
- CSL-2004-GanzingerK #equation #proving #reasoning #theorem proving
- Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.
- IJCAR-2004-GanzingerSW #composition #proving #similarity
- Modular Proof Systems for Partial Functions with Weak Equality (HG, VSS, UW), pp. 168–182.
- CADE-2003-GanzingerHW
- Superposition Modulo a Shostak Theory (HG, TH, UW), pp. 182–196.
- CADE-2003-GanzingerS #equivalence #normalisation #reasoning
- Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation (HG, JS), pp. 335–349.
- LICS-2003-GanzingerK #proving #theorem proving
- New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.
- CADE-2002-Ganzinger
- Shostak Light (HG), pp. 332–346.
- ICLP-2002-GanzingerM #algorithm #logic
- Logical Algorithms (HG, DAM), pp. 209–223.
- IJCAR-2001-GanzingerM #bottom-up #logic programming #source code #theorem
- A New Meta-complexity Theorem for Bottom-Up Logic Programs (HG, DAM), pp. 514–528.
- IJCAR-2001-GanzingerNN
- Context Trees (HG, RN, PN), pp. 242–256.
- LICS-2001-Ganzinger #concept #decidability #problem #semantics #word
- Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems (HG), pp. 81–90.
- POPL-2001-Ganzinger #deduction #performance #program analysis
- Efficient deductive methods for program analysis (HG), pp. 102–103.
- ICALP-1999-CortierGJV #decidability #reachability
- Decidable Fragments of Simultaneous Rigid Reachability (VC, HG, FJ, MV), pp. 250–260.
- LICS-1999-GanzingerMV #transitive
- The Two-Variable Guarded Fragment with Transitive Relations (HG, CM, MV), pp. 24–34.
- LICS-1999-GanzingerN #similarity
- A Superposition Decision Procedure for the Guarded Fragment with Equality (HG, HdN), pp. 295–303.
- CADE-1998-BachmairG #strict
- Strict Basic Superposition (LB, HG), pp. 160–174.
- CADE-1998-BachmairGV #constraints #similarity
- Elimination of Equality via Transformation with Ordering Constraints (LB, HG, AV), pp. 175–190.
- CADE-1997-GanzingerMW #order #type system
- Soft Typing for Ordered Resolution (HG, CM, CW), pp. 321–335.
- CADE-1996-Ganzinger #proving #theorem proving
- Saturation-Based Theorem Proving: Past Successes and Future Potential (HG), p. 1.
- CADE-1996-GanzingerW #monad #proving #theorem proving
- Theorem Proving in Cancellative Abelian Monoids (HG, UW), pp. 388–402.
- ICALP-1996-Ganzinger #proving #theorem proving
- Saturation-Based Theorem Proving (HG), pp. 1–3.
- LICS-1996-BasinG #analysis #complexity #order
- Complexity Analysis Based on Ordered Resolution (DAB, HG), pp. 456–465.
- CADE-1994-BachmairG #order
- Ordered Chaining for Total Orderings (LB, HG), pp. 435–450.
- LICS-1994-BachmairG #transitive
- Rewrite Techniques for Transitive Relations (LB, HG), pp. 384–393.
- ALP-1992-BachmairGW #first-order #proving #theorem proving
- Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
- CADE-1992-BachmairGLS
- Basic Paramodulation and Superposition (LB, HG, CL, WS), pp. 462–476.
- ICLP-1991-BachmairG #logic programming #semantics #similarity #source code
- Perfect Model Semantics for Logic Programs with Equality (LB, HG), pp. 645–659.
- CADE-1990-BachmairG #on the #order #strict
- On Restrictions of Ordered Paramodulation with Simplification (LB, HG), pp. 427–441.
- ICSE-1990-GanzingerS #composition #horn clause #order #specification
- System Support for Modular Order-Sorted Horn Clause Specifications (HG, RS), pp. 150–159.
- RTA-1989-BertlingG #optimisation
- Completion-Time Optimization of Rewrite-Time Goal Solving (HB, HG), pp. 45–58.
- ESOP-1988-BertlingGS #equation #named #specification
- CEC: A System for the Completion of Conditional Equational Specifications (HB, HG, RS), pp. 378–379.
- SLP-1985-GanzingerH85 #compilation #composition #logic programming
- Modular Logic Programming of Compilers (HG, MH), pp. 242–253.
- SCC-1984-GanzingerG #attribute grammar
- Attribute coupled grammars (HG, RG), pp. 157–170.
- ICALP-1983-Ganzinger #compilation #composition #data type #semantics
- Modular Compiler Descriptions Based on Abstract Semantic Data Types (HG), pp. 237–249.
- SCC-1982-GanzingerGMW #compilation #generative #semantics
- A Truly Generative Semantics-Directed Compiler Generator (HG, RG, UM, RW), pp. 172–184.
- SDCG-1980-Ganzinger #attribute grammar #semantics
- Transforming denotational semantics into practical attribute grammars (HG), pp. 1–69.
- ICSE-1976-WilhelmRCGLN #compilation #design #evaluation #generative
- Design Evaluation of the Compiler Generating System MUGI (RW, KR, JC, HG, WL, RN), pp. 571–576.
- CAAP-1989-Ganzinger #order
- Order-Sorted Completion: The Many-Sorted Way (Extended Abstract) (HG), pp. 244–258.