Database Entry Point
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template, generated: 14:19, 23 September 2014

Search the publication database

  . Return

Your search returned the following 58 documents:

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