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

MPI-INF RG1 Publications, generated: 5:31, 23 October 2019

Search the publication database

  . Return

Your search returned the following 15 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'06), Phnom Penh, Cambodia, 2006, 497-511
  3. 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
  4. 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]
  5. 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]
  6. 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]
  7. 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
  8. 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.
  9. 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
  10. 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
  11. Harald Ganzinger
    The Saturate System
    . Note: Available on the World-Wide Web and URL http://www.mpi-sb.mpg.de/SATURATE/Saturate.html
  12. 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
  13. 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
  14. 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
  15. 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)