Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
Leo Bachmair
2000 – 2009
- 2005
[c37]Paul Agron, Leo Bachmair, Frank Nielsen: A Visual Interactive Framework for Formal Derivation. International Conference on Computational Science (1) 2005: 1019-1026- 2004
- [c36]Christelle Scharff, Leo Bachmair: On the Combination of Congruence Closure and Completion. AISC 2004: 103-117
- 2003
- [j10]Leo Bachmair, Ashish Tiwari, Laurent Vigneron: Abstract Congruence Closure. J. Autom. Reasoning 31(2): 129-168 (2003)
- 2001
- [p1]Leo Bachmair, Harald Ganzinger: Resolution Theorem Proving. Handbook of Automated Reasoning 2001: 19-99
- 2000
- [c35]
- [c34]
- [c33]Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, Laurent Vigneron: Congruence Closure Modulo Associativity and Commutativity. FroCoS 2000: 245-259
- [e1]Leo Bachmair (Ed.): Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings. Lecture Notes in Computer Science 1833, Springer 2000, ISBN 3-540-67778-X
1990 – 1999
- 1999
- [c32]Leo Bachmair, C. R. Ramakrishnan, I. V. Ramakrishnan, Ashish Tiwari: Normalization via Rewrite Closures. RTA 1999: 190-204
- 1998
- [j9]Leo Bachmair, Harald Ganzinger: Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6): 1007-1049 (1998)
- [c31]
- [c30]Leo Bachmair, Harald Ganzinger, Andrei Voronkov: Elimination of Equality via Transformation with Ordering Constraints. CADE 1998: 175-190
- [c29]Maxim Lifantsev, Leo Bachmair: An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction. TPHOLs 1998: 277-293
- 1997
- [c28]
- [c27]Leo Bachmair, Ashish Tiwari: D-Bases for Polynomial Ideals over Commutative Noetherian Rings. RTA 1997: 113-127
- 1996
- [c26]Leo Bachmair, Ta Chen, C. R. Ramakrishnan, I. V. Ramakrishnan: Subsumption Algorithms Based on Search Trees. CAAP 1996: 135-148
- 1995
- [j8]Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation. Inf. Comput. 121(2): 172-192 (1995)
- [c25]Leo Bachmair, Ta Chen, I. V. Ramakrishnan, Siva Anantharaman, Jacques Chabin: Experiments with Associative-Commutative Discrimination Nets. IJCAI 1995: 348-355
- 1994
- [j7]Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5: 193-212 (1994)
- [j6]Leo Bachmair, Nachum Dershowitz: Equational Inference, Canonical Proofs, and Proof Orderings. J. ACM 41(2): 236-276 (1994)
- [j5]Leo Bachmair, Harald Ganzinger: Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. 4(3): 217-247 (1994)
- [c24]
- [c23]Leo Bachmair, Harald Ganzinger: Buchberger's Algorithm: A Constraint-Based Completion Procedure. CCL 1994: 285-301
- [c22]Leo Bachmair, Harald Ganzinger, Jürgen Stuber: Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings. COMPASS/ADT 1994: 1-29
- [c21]
- [c20]
- 1993
- [c19]Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. Kurt Gödel Colloquium 1993: 83-96
- [c18]Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Set Constraints are the Monadic Class. LICS 1993: 75-83
- [c17]
- [c16]Leo Bachmair, Ta Chen, I. V. Ramakrishnan: Associative-Commutative Discrimination Nets. TAPSOFT 1993: 61-74
- 1992
- [j4]
- [c15]Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Theorem Proving for Hierarchic First-Order Theories. ALP 1992: 420-434
- [c14]Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation and Superposition. CADE 1992: 462-476
- [c13]Leo Bachmair, Harald Ganzinger: Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. LPAR 1992: 273-284
- 1991
- [c12]Leo Bachmair, Harald Ganzinger: Perfect Model Semantics for Logic Programs with Equality. ICLP 1991: 645-659
- 1990
- [c11]Leo Bachmair, Harald Ganzinger: On Restrictions of Ordered Paramodulation with Simplification. CADE 1990: 427-441
- [c10]Leo Bachmair, Harald Ganzinger: Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). CTRS 1990: 162-180
1980 – 1989
- 1989
- [j3]Leo Bachmair, Nachum Dershowitz: Completion for Rewriting Modulo a Congruence. Theor. Comput. Sci. 67(2&3): 173-201 (1989)
- [c9]
- 1988
- [j2]Leo Bachmair, Nachum Dershowitz: Critical Pair Criteria for Completion. J. Symb. Comput. 6(1): 1-18 (1988)
- [c8]
- 1987
- [c7]Leo Bachmair, Nachum Dershowitz: A critical pair criterion for completion modulo a congruence. EUROCAL 1987: 452-453
- [c6]Leo Bachmair, Nachum Dershowitz: Inference Rules for Rewrite-Based First-Order Theorem Proving. LICS 1987: 331-337
- [c5]
- 1986
- [c4]
- [c3]Leo Bachmair, Nachum Dershowitz: Critical-pair criteria for the Knuth-Bendix completion procedure. SYMSAC 1986: 215-217
- [c2]
- 1985
- [j1]Leo Bachmair, David A. Plaisted: Termination Orderings for Associative-Commutative Rewriting Systems. J. Symb. Comput. 1(4): 329-349 (1985)
- [c1]
Coauthor Index
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-02-15 22:13 CET by the dblp team