|
Search the dblp DataBase
Leo Bachmair:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
Publications of Author
- Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder
Basic Paramodulation and Superposition. [Citation Graph (1, 0)][DBLP] CADE, 1992, pp:462-476 [Conf]
- Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Set Constraints are the Monadic Class [Citation Graph (1, 0)][DBLP] LICS, 1993, pp:75-83 [Conf]
- Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder
Basic Paramodulation [Citation Graph (1, 0)][DBLP] Inf. Comput., 1995, v:121, n:2, pp:172-192 [Journal]
- Leo Bachmair, Harald Ganzinger
Rewrite-Based Equational Theorem Proving with Selection and Simplification. [Citation Graph (1, 0)][DBLP] J. Log. Comput., 1994, v:4, n:3, pp:217-247 [Journal]
- Christelle Scharff, Leo Bachmair
On the Combination of Congruence Closure and Completion. [Citation Graph (0, 0)][DBLP] AISC, 2004, pp:103-117 [Conf]
- Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Theorem Proving for Hierarchic First-Order Theories. [Citation Graph (0, 0)][DBLP] ALP, 1992, pp:420-434 [Conf]
- Leo Bachmair, Ta Chen, C. R. Ramakrishnan, I. V. Ramakrishnan
Subsumption Algorithms Based on Search Trees. [Citation Graph (0, 0)][DBLP] CAAP, 1996, pp:135-148 [Conf]
- Leo Bachmair, Nachum Dershowitz
Commutation, Transformation, and Termination. [Citation Graph (0, 0)][DBLP] CADE, 1986, pp:5-20 [Conf]
- Leo Bachmair, Harald Ganzinger
On Restrictions of Ordered Paramodulation with Simplification. [Citation Graph (0, 0)][DBLP] CADE, 1990, pp:427-441 [Conf]
- Leo Bachmair, Harald Ganzinger
Ordered Chaining for Total Orderings. [Citation Graph (0, 0)][DBLP] CADE, 1994, pp:435-450 [Conf]
- Leo Bachmair, Harald Ganzinger
Strict Basic Superposition. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:160-174 [Conf]
- Leo Bachmair, Harald Ganzinger, Andrei Voronkov
Elimination of Equality via Transformation with Ordering Constraints. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:175-190 [Conf]
- Leo Bachmair, Ashish Tiwari
Abstract Congruence Closure and Specializations. [Citation Graph (0, 0)][DBLP] CADE, 2000, pp:64-78 [Conf]
- Ashish Tiwari, Leo Bachmair, Harald Rueß
Rigid E-Unification Revisited. [Citation Graph (0, 0)][DBLP] CADE, 2000, pp:220-234 [Conf]
- Leo Bachmair, Harald Ganzinger
Buchberger's Algorithm: A Constraint-Based Completion Procedure. [Citation Graph (0, 0)][DBLP] CCL, 1994, pp:285-301 [Conf]
- Leo Bachmair, Harald Ganzinger, Jürgen Stuber
Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings. [Citation Graph (0, 0)][DBLP] COMPASS/ADT, 1994, pp:1-29 [Conf]
- Leo Bachmair, Harald Ganzinger
Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). [Citation Graph (0, 0)][DBLP] CTRS, 1990, pp:162-180 [Conf]
- Leo Bachmair, Harald Ganzinger
Associative-Commutative Superposition. [Citation Graph (0, 0)][DBLP] CTRS, 1994, pp:1-14 [Conf]
- Leo Bachmair, Nachum Dershowitz
A critical pair criterion for completion modulo a congruence. [Citation Graph (0, 0)][DBLP] EUROCAL, 1987, pp:452-453 [Conf]
- Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, Laurent Vigneron
Congruence Closure Modulo Associativity and Commutativity. [Citation Graph (0, 0)][DBLP] FroCos, 2000, pp:245-259 [Conf]
- Paul Agron, Leo Bachmair, Frank Nielsen
A Visual Interactive Framework for Formal Derivation. [Citation Graph (0, 0)][DBLP] International Conference on Computational Science (1), 2005, pp:1019-1026 [Conf]
- Leo Bachmair, Harald Ganzinger
Perfect Model Semantics for Logic Programs with Equality. [Citation Graph (0, 0)][DBLP] ICLP, 1991, pp:645-659 [Conf]
- Leo Bachmair, Ta Chen, I. V. Ramakrishnan, Siva Anantharaman, Jacques Chabin
Experiments with Associative-Commutative Discrimination Nets. [Citation Graph (0, 0)][DBLP] IJCAI, 1995, pp:348-355 [Conf]
- Leo Bachmair
Paramodulation, Superposition, and Simplification. [Citation Graph (0, 0)][DBLP] Kurt Gödel Colloquium, 1997, pp:1-3 [Conf]
- Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. [Citation Graph (0, 0)][DBLP] Kurt Gödel Colloquium, 1993, pp:83-96 [Conf]
- Leo Bachmair
Proof by Consistency in Equational Theories [Citation Graph (0, 0)][DBLP] LICS, 1988, pp:228-233 [Conf]
- Leo Bachmair, Nachum Dershowitz
Inference Rules for Rewrite-Based First-Order Theorem Proving [Citation Graph (0, 0)][DBLP] LICS, 1987, pp:331-337 [Conf]
- Leo Bachmair, Nachum Dershowitz, Jieh Hsiang
Orderings for Equational Proofs [Citation Graph (0, 0)][DBLP] LICS, 1986, pp:346-357 [Conf]
- Leo Bachmair, Harald Ganzinger
Rewrite Techniques for Transitive Relations [Citation Graph (0, 0)][DBLP] LICS, 1994, pp:384-393 [Conf]
- Leo Bachmair, Harald Ganzinger
Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. [Citation Graph (0, 0)][DBLP] LPAR, 1992, pp:273-284 [Conf]
- Leo Bachmair
Proof Normalization for Resolution and Paramodulation. [Citation Graph (0, 0)][DBLP] RTA, 1989, pp:15-28 [Conf]
- Leo Bachmair
Rewrite Techniques in Theorem Proving (Abstract). [Citation Graph (0, 0)][DBLP] RTA, 1993, pp:1- [Conf]
- Leo Bachmair, Nachum Dershowitz
Completion for Rewriting Modulo a Congruence. [Citation Graph (0, 0)][DBLP] RTA, 1987, pp:192-203 [Conf]
- Leo Bachmair, David A. Plaisted
Associative Path Orderings. [Citation Graph (0, 0)][DBLP] RTA, 1985, pp:241-254 [Conf]
- Leo Bachmair, C. R. Ramakrishnan, I. V. Ramakrishnan, Ashish Tiwari
Normalization via Rewrite Closures. [Citation Graph (0, 0)][DBLP] RTA, 1999, pp:190-204 [Conf]
- Leo Bachmair, Ashish Tiwari
D-Bases for Polynomial Ideals over Commutative Noetherian Rings. [Citation Graph (0, 0)][DBLP] RTA, 1997, pp:113-127 [Conf]
- Leo Bachmair, Ta Chen, I. V. Ramakrishnan
Associative-Commutative Discrimination Nets. [Citation Graph (0, 0)][DBLP] TAPSOFT, 1993, pp:61-74 [Conf]
- Maxim Lifantsev, Leo Bachmair
An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction. [Citation Graph (0, 0)][DBLP] TPHOLs, 1998, pp:277-293 [Conf]
- Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Refutational Theorem Proving for Hierachic First-Order Theories. [Citation Graph (0, 0)][DBLP] Appl. Algebra Eng. Commun. Comput., 1994, v:5, n:, pp:193-212 [Journal]
- Leo Bachmair
Associative-Commutative Reduction Orderings. [Citation Graph (0, 0)][DBLP] Inf. Process. Lett., 1992, v:43, n:1, pp:21-27 [Journal]
- Leo Bachmair, Nachum Dershowitz
Equational Inference, Canonical Proofs, and Proof Orderings. [Citation Graph (0, 0)][DBLP] J. ACM, 1994, v:41, n:2, pp:236-276 [Journal]
- Leo Bachmair, Harald Ganzinger
Ordered Chaining Calculi for First-Order Theories of Transitive Relations. [Citation Graph (0, 0)][DBLP] J. ACM, 1998, v:45, n:6, pp:1007-1049 [Journal]
- Leo Bachmair, Ashish Tiwari, Laurent Vigneron
Abstract Congruence Closure. [Citation Graph (0, 0)][DBLP] J. Autom. Reasoning, 2003, v:31, n:2, pp:129-168 [Journal]
- Leo Bachmair, Nachum Dershowitz
Critical Pair Criteria for Completion. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 1988, v:6, n:1, pp:1-18 [Journal]
- Leo Bachmair, David A. Plaisted
Termination Orderings for Associative-Commutative Rewriting Systems. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 1985, v:1, n:4, pp:329-349 [Journal]
- Leo Bachmair, Nachum Dershowitz
Completion for Rewriting Modulo a Congruence. [Citation Graph (0, 0)][DBLP] Theor. Comput. Sci., 1989, v:67, n:2&3, pp:173-201 [Journal]
Search in 0.041secs, Finished in 0.044secs
|