max planck institut
informatik

# 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
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
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
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)