Your search returned the following 58 documents:

58. Modular Proof Systems for Partial Functions with Evans Equality
    Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldmann
    Information and Computation 204 (10): 1453-1492, 2006
    
57. Theory Instantiation
    Harald Ganzinger and Konstantin Korovin
    In: Logic for Programming, Artificial Intelligence, and Reasoning : 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, 2006, 497-511
    
56. Theory Instantiation
    Harald Ganzinger and Konstantin Korovin
    In: 13th Conference on Logic for Programming Artificial Intelligence Reasoning (LPAR'06), Phnom Penh, Cambodia, 2006, 497-511
    
55. Superposition with equivalence reasoning and delayed clause normal form transformation
    Harald Ganzinger and Jürgen Stuber
    Information and Computation 199 (1-2): 3-23, 2005
    
54. Fast Term Indexing with Coded Context Trees
    Harald Ganzinger, Robert Nieuwenhuis, and Pilar Nivela
    Journal of Automated Reasoning 32 (2): 103-120, 2004
    [PS: Download: 2003JAR.ps]
    
53. Integration of equational reasoning into instantiation-based theorem proving
    Harald Ganzinger and Konstantin Korovin
    In: Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, 2004, 71-84
    
52. Modular Proof Systems for Partial Functions with Weak Equality
    Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldmann
    In: Automated reasoning : Second International Joint Conference, IJCAR 2004, Cork, Ireland, 2004, 168-182
    
51. DPLL(T): Fast Decision Procedures
    Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
    In: Computer aided verification : 16th International Conference, CAV 2004, Boston, Massachusetts, 2004, 175-188
    
50. New Directions in Instantiation-Based Theorem Proving
    Harald Ganzinger and Konstantin Korovin
    In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), Ottawa, Canada, old, 2003, 55-64
    [PDF: Download: _03LICS.pdf]
    
49. Superposition modulo a Shostak Theory
    Harald Ganzinger, Thomas Hillenbrand, and Uwe Waldmann
    In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, Miami, Florida, July, 30 - August, 2, 2003, 182-196
    [PS: Download: _03CADE.2.ps]
    
48. Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
    Harald Ganzinger and Jürgen Stuber
    In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, Miami, Florida, 666, 2003, 335-349
    [PS: Download: _03CADE.1.ps]
    
47. Logical Algorithms
    Harald Ganzinger and David McAllester
    In: Logic Programming. 18th International Conference, ICLP 2002, Copenhagen, Denmark, 2002, 209-223
    [PDF: Download: _02ICLP.pdf]
    
46. Shostak Light
    Harald Ganzinger
    In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, 2002, 332-346
    [PDF: Download: _02CADE.pdf]
    
45. A new meta-complexity theorem for bottom-up logic programs
    Harald Ganzinger and David McAllester
    In: Automated reasoning : First International Joint Conference, IJCAR 2001, Siena, Italy, 2001, 514-528
    [PDF: Download: _01IJCAR-2.pdf]
    
44. A Resolution-Based Decision Procedure for Extensions of K4
    Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, and Renate A. Schmidt
    In: Advances in Modal Logic, Volume 2, 2001, 225-246
    [PS: Download: _01AIML.ps.gz]
    
43. Automated Complexity Analysis Based on Ordered Resolution
    David A. Basin and Harald Ganzinger
    Journal of the ACM 48 (1): 70-109, 2001
    [PS: Download: 2001JACM.ps.gz]
    
42. Bottom-Up Deduction with Deletion and Priorities
    Harald Ganzinger
    In: Programs as Data Objects (PADO-01) : Second Symposium PADO 2001, Aarhus, Denmark, May, 21-23, 2001, 2001, 276-277
    
41. Constraints and Theorem Proving
    Harald Ganzinger and Robert Nieuwenhuis
    In: Contraints in Computational Logics, International Summer School (CCL-99), Gif-sur-Yvette, France, 2001, 159-201
    [PS: Download: 2001CCL.ps.gz] [Download: 2001CCL.dvi]
    
40. Context trees
    Harald Ganzinger, Robert Nieuwenhuis, and Pilar Nivela
    In: Automated reasoning : First International Joint Conference, IJCAR 2001, Siena, Italy, 2001, 242-256
    [PDF: Download: _01IJCAR-1.pdf]
    
39. Efficient deductive methods for program analysis
    Harald Ganzinger
    ACM SIGPLAN Notices 36 (3): 102-103, 2001
    
38. Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems
    Harald Ganzinger
    In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS-01), Boston, USA, 2001, 81-90
    [PS: Download: _01LICS.ps.gz]
    
37. Resolution Theorem Proving
    Leo Bachmair and Harald Ganzinger
    In: Handbook of Automated Reasoning, 2001, 19-99
    [PS: Download: 2001Handbook.ps.gz]
    
36. Chaining Techniques for Automated Theorem Proving in Many-Valued Logics
    Harald Ganzinger and Viorica Sofronie-Stokkermans
    In: Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL-00), Portland, Oregon, May, 23 - 25, 2000, 337-344
    [PS: Download: _00ISMVL_ps.gz]
    
35. Rigid Reachability: The Non-Symmetric Form of Rigid E-unification
    Harald Ganzinger, Florent Jacquemard, and Margus Veanes
    International Journal of Foundations of Computer Science 11 (1): 3-27, 2000
    
34. A Superposition Decision Procedure for the Guarded Fragment with Equality
    Harald Ganzinger and Hans de Nivelle
    In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99), Trento, Italy, Trento, Italy, 1999, 295-303
    [PDF: Download: 99LICS_2.pdf] [PS: Download: 99LICS_2_ps.gz]
    
33. Decidable fragments of simultaneous rigid reachability
    V. Cortier, Harald Ganzinger, Florent Jacquemard, and Margus Veanes
    In: Proceedings of the 26th International Colloquium on Automata, Languages and Programming (ICALP-99), Prague, Czech Republik, July 11-15, 1999, 1999, 250-260. Note: Full version of this paper is available as MPI Research Report MPI-I-1999-2-004.
    
32. The Two-Variable Guarded Fragment with Transitive Relations
    Harald Ganzinger, Christoph Meyer, and Margus Veanes
    In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99), Trento, Italy, Trento, Italy, 1999, 24-34
    
31. Elimination of Equality via Transformation with Ordering Constraints
    Leo Bachmair, Harald Ganzinger, and Andrei Voronkov
    In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5-10 1998, 1998, 175-190. Note: Short version of MPI-I-97-2-012
    
30. Equational Reasoning in Saturation-Based Theorem Proving
    Leo Bachmair and Harald Ganzinger
    In: Automated Deduction: A Basis for Applications, 1998, 353-397
    
29. Ordered Chaining Calculi for First-Order Theories of Transitive Relations
    Leo Bachmair and Harald Ganzinger
    Journal of the ACM 45 (6): 1007-1049, 1998. Note: Revised Version of MPI-I-95-2-009.
    
28. Preface
    Harald Ganzinger
    Theoretical Computer Science 208 (1/2): 1 p., 1998
    
27. Rigid Reachability
    Harald Ganzinger, Florent Jacquemard, and Margus Veanes
    In: Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN-98), Manila, The Philippines,, December, 8-10, 1998, 1998, 4-21. Note: A full version of this paper is available as MPI-I Research Report MPI-I-98-2-013.
    
26. Strict Basic Superposition
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5-10 1998, 1998, 160-174
    
25. Soft Typing for Ordered Resolution
    Harald Ganzinger, Christoph Meyer, and Christoph Weidenbach
    In: Proceedings of the 14th International Conference on Automated Deduction (CADE-14), Townsville, Australia, July, 14-17, 1997, 321-335
    
24. Complexity Analysis Based on Ordered Resolution
    David A. Basin and Harald Ganzinger
    In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS'96), New Brunswick, New Jersey, USA, July 27-30, 1996, 1996, 456-465
    
23. Saturation-based theorem proving (abstract)
    Harald Ganzinger
    In: Automata, Languages and Programming: International Colloquium (ICALP-23), Paderborn, Germany, July, 8-12, 1996, 1-3
    
22. Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)
    Harald Ganzinger and Uwe Waldmann
    In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), New Brunswick, USA, July, 30 - August, 3, 1996, 388-402. Note: Full version: Technical Report MPI-I-96-2-001, Max-Planck-Institut für Informatik, Saarbrücken, Germany, January 1996.
    
21. Associative-Commutative Superposition
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), Jerusalem, Israel, July, 13-15, 1994, 1995, 1-14. Note: Revised version of MPI-I-93-267, 1993
    
20. Basic Paramodulation
    Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder
    Information and Computation 121 (2): 172-192, 1995. Note: Revised version of TR MPI-I-93-236, 1993
    
19. Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings
    Leo Bachmair, Harald Ganzinger, and Jürgen Stuber
    In: Recent Trends in Data Type Specification. 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May/June 1994, 1995, 1-29
    
18. Buchberger's algorithm: a constraint-based completion procedure
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), Munich, Germany, September 7-9, 1994, 1994, 285-301
    
17. Ordered Chaining for Total Orderings
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), Nancy, France, June 26 - July 1, 1994, 1994, 435-450. Note: Full version available as Research Report MPI-I-93-250, 1993
    
16. Refutational Theorem Proving for Hierarchic First-Order Theories
    Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
    Applicable Algebra in Engineering, Communication and Computing (AAECC) 5 (3/4): 193-212, 1994. Note: Earlier Version: Theorem Proving for Hierarchic First-Order Theories, in Giorgio Levi and H{\'e}l{\`e}ne Kirchner, editors, {\em Algebraic and Logic Programming, Third International Conference}, LNCS 632, pages 420--434, Volterra, Italy, September 2--4, 1992, Springer-Verlag
    
15. Rewrite-based equational theorem proving with selection and simplification
    Leo Bachmair and Harald Ganzinger
    Journal of Logic and Computation 4 (3): 217-247, 1994. Note: Revised version of Technical Report MPI-I-91-208, 1991
    
14. Rewrite Techniques for Transitive Relations
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, Paris, France, 1994, 384-393. Note: Full version available as Technical Report MPI-I-93-249
    
13. The Saturate System
    Harald Ganzinger
    . Note: Available on the World-Wide Web and URL http://www.mpi-sb.mpg.de/SATURATE/Saturate.html
    
12. Completion Subsystem
    Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, and Fernando Orejas
    In: Program Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System, 1993, 460-494
    
11. Set Constraints are the Monadic Class
    Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
    In: Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, June 19-23, 1993, 1993, 75-83
    
10. Superposition with simplification as a decision procedure for the monadic class with equality
    Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
    In: Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, 1993, 83-96. Note: Revised version of Technical Report MPI-I-93-204
    
9. Basic Paramodulation and Superposition
   Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder
   In: Proceedings of the 11th International Conference on Automated Deduction (CADE-11), Saratoga Springs, NY, 1992, 1992, 462-476
   
8. Inductive theorem proving by consistency for first-order clauses
   Harald Ganzinger and Jürgen Stuber
   In: Informatik - Festschrift zum 60. Geburtstag von Günter Hotz, 1992, 441-462. Note: Also in Proc.~CTRS'92, LNCS~656, pp.~226--241
   
7. Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
   Leo Bachmair and Harald Ganzinger
   In: Logic Programming and Automated Reasoning, St.\ Petersburg, Russia, 1992, 1992, 273-284
   
6. Termination Proofs of Well-Moded Logic Programs Via Conditional Rewrite Systems
   Harald Ganzinger and Uwe Waldmann
   In: Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems '92, 1992, 430-437
   
5. Theorem proving for hierarchic first-order theories
   Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
   In: Algebraic and Logic Programming, 1992, 420-434. Note: Revised version in AAECC, vol.\ 5, number 3/4, pp.\ 193--212, 1994)
   
4. A completion procedure for conditional equations
   Harald Ganzinger
   Journal of Symbolic Computation 11: 51-81, 1991
   
3. Completion of first-order clauses with equality by strict superposition
   Leo Bachmair and Harald Ganzinger
   In: Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting, Montreal, Canada, 1990, 1991, 162-180
   
2. Order-Sorted Completion: The Many-Sorted Way
   Harald Ganzinger
   Theoretical Computer Science 89: 3-32, 1991
   
1. Perfect model semantics for logic programs with equality
   Leo Bachmair and Harald Ganzinger
   In: Proceedings International Conference on Logic Programming '91, Paris, France, 1991, 1991, 645-659