Fast Term Indexing with Coded Context Trees
Ganzinger, H. and Nieuwenhuis, R. and Nivela, P.
Automated Complexity Analysis Based on Ordered Resolution
Basin, D. and Ganzinger, H.
Resolution Theorem Proving
Bachmair, L. and Ganzinger, H.
Constraints and Theorem Proving
Ganzinger, H. and Nieuwenhuis, R.
Rigid Reachability: The Non-Symmetric Form of Rigid {E}-Unification
H. Ganzinger and F. Jacquemard and M. Veanes
Equational Reasoning in Saturation-Based Theorem Proving
Bachmair, L. and Ganzinger, H.
Ordered Chaining Calculi for First-Order Theories of Transitive Relations
Bachmair, L. and Ganzinger, H.
Basic Paramodulation
Bachmair, L. and Ganzinger, H. and Lynch, Chr. and Snyder, W.
Refutational Theorem Proving for Hierarchic First-Order Theories
Bachmair, Leo and Ganzinger, Harald and Waldmann, Uwe
[an error occurred while processing this directive]