New Directions in Instantiation-Based Theorem Proving
Ganzinger, H. and Korovin, K.
Superposition modulo a {S}hostak theory
Ganzinger, H. and Hillenbrand, T. and Waldmann, U.
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
Ganzinger, H. and Stuber, J.
Logical Algorithms
Ganzinger, H. and McAllester, D.
Shostak Light
Ganzinger, H.
Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems
Ganzinger, H.
A new meta-complexity theorem for bottom-up logic programs
Ganzinger, H. and McAllester, D.
Context trees
Ganzinger, H. and Nieuwenhuis, R. and Nivela, P.
A Resolution-Based Decision Procedure for Extensions of K4
Ganzinger, Harald and Hustadt, Ullrich and Meyer, Christoph and Schmidt, Renate A.
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics
Ganzinger, H. and Sofronie-Stokkermans, V.
A Superposition Decision Procedure for the Guarded Fragment with Equality
Ganzinger, H. and De Nivelle, H.
The Two-Variable Guarded Fragment with Transitive Relations
Ganzinger, H. and Meyer, Chr. and Veanes, M.
Decidable fragments of simultaneous rigid reachability
Cortier, V. and Ganzinger, H. and Jacquemard, F. and Veanes, M.
Strict Basic Superposition
Bachmair, L. and Ganzinger, H.
Elimination of Equality via Transformation with Ordering Constraints
Bachmair, L. and Ganzinger, H. and Voronkov, A.
Rigid Reachability
Ganzinger, H. and Jacquemard, F. and Veanes, M.
Soft typing for ordered resolution
Ganzinger, H. and Meyer, Chr. and Weidenbach, Chr.
Complexity Analysis Based on Ordered Resolution
Basin, D. and Ganzinger, H.
Theorem Proving in Cancellative Abelian Monoids
Ganzinger, H. and Waldmann, U.
Rewrite Techniques for Transitive Relations
Bachmair, L. and Ganzinger, H.
Associative-Commutative Superposition
Bachmair, L. and Ganzinger, H.
Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings
Bachmair, L. and Ganzinger, H. and Stuber, J.
Buchberger's algorithm: a constraint-based completion procedure
Bachmair, L. and Ganzinger, H.
Ordered Chaining for Total Orderings
Bachmair, L. and Ganzinger, H.
[an error occurred while processing this directive]