default search action
Leo Bachmair
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
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
- [j11]Leo Bachmair, Ashish Tiwari, Laurent Vigneron:
Abstract Congruence Closure. J. Autom. Reason. 31(2): 129-168 (2003) - 2001
- [p1]Leo Bachmair, Harald Ganzinger:
Resolution Theorem Proving. Handbook of Automated Reasoning 2001: 19-99 - 2000
- [c35]Leo Bachmair, Ashish Tiwari:
Abstract Congruence Closure and Specializations. CADE 2000: 64-78 - [c34]Ashish Tiwari, Leo Bachmair, Harald Rueß:
Rigid E-Unification Revisited. CADE 2000: 220-234 - [c33]Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, Laurent Vigneron:
Congruence Closure Modulo Associativity and Commutativity. FroCoS 2000: 245-259 - [e1]Leo Bachmair:
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 [contents]
1990 – 1999
- 1999
- [c32]Leo Bachmair, C. R. Ramakrishnan, I. V. Ramakrishnan, Ashish Tiwari:
Normalization via Rewrite Closures. RTA 1999: 190-204 - 1998
- [j10]Leo Bachmair, Harald Ganzinger:
Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6): 1007-1049 (1998) - [c31]Leo Bachmair, Harald Ganzinger:
Strict Basic Superposition. CADE 1998: 160-174 - [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]Leo Bachmair:
Paramodulation, Superposition, and Simplification. Kurt Gödel Colloquium 1997: 1-3 - [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
- [j9]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
- [j8]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5: 193-212 (1994) - [j7]Leo Bachmair, Nachum Dershowitz:
Equational Inference, Canonical Proofs, and Proof Orderings. J. ACM 41(2): 236-276 (1994) - [j6]Leo Bachmair, Harald Ganzinger:
Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. 4(3): 217-247 (1994) - [c24]Leo Bachmair, Harald Ganzinger:
Ordered Chaining for Total Orderings. CADE 1994: 435-450 - [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]Leo Bachmair, Harald Ganzinger:
Associative-Commutative Superposition. CTRS 1994: 1-14 - [c20]Leo Bachmair, Harald Ganzinger:
Rewrite Techniques for Transitive Relations. LICS 1994: 384-393 - 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]Leo Bachmair:
Rewrite Techniques in Theorem Proving (Abstract). RTA 1993: 1 - [c16]Leo Bachmair, Ta Chen, I. V. Ramakrishnan:
Associative-Commutative Discrimination Nets. TAPSOFT 1993: 61-74 - 1992
- [j5]Leo Bachmair:
Associative-Commutative Reduction Orderings. Inf. Process. Lett. 43(1): 21-27 (1992) - [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
- [j4]Leo Bachmair, Nachum Dershowitz:
Completion for Rewriting Modulo a Congruence. Theor. Comput. Sci. 67(2&3): 173-201 (1989) - [c9]Leo Bachmair:
Proof Normalization for Resolution and Paramodulation. RTA 1989: 15-28 - 1988
- [j3]Leo Bachmair, Nachum Dershowitz:
Critical Pair Criteria for Completion. J. Symb. Comput. 6(1): 1-18 (1988) - [c8]Leo Bachmair:
Proof by Consistency in Equational Theories. LICS 1988: 228-233 - 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]Leo Bachmair, Nachum Dershowitz:
Completion for Rewriting Modulo a Congruence. RTA 1987: 192-203 - 1986
- [c4]Leo Bachmair, Nachum Dershowitz:
Commutation, Transformation, and Termination. CADE 1986: 5-20 - [c3]Leo Bachmair, Nachum Dershowitz:
Critical-pair criteria for the Knuth-Bendix completion procedure. SYMSAC 1986: 215-217 - [c2]Leo Bachmair, Nachum Dershowitz, Jieh Hsiang:
Orderings for Equational Proofs. LICS 1986: 346-357 - 1985
- [j2]Leo Bachmair, David A. Plaisted:
Termination Orderings for Associative-Commutative Rewriting Systems. J. Symb. Comput. 1(4): 329-349 (1985) - [c1]Leo Bachmair, David A. Plaisted:
Associative Path Orderings. RTA 1985: 241-254 - 1980
- [j1]Leo Bachmair, Bruno Buchberger:
A simplified proof of the characterization theorem for Gröbner-bases. SIGSAM Bull. 14(4): 29-34 (1980)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 22:46 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: