Leo Bachmair

According to our database, Leo Bachmair authored at least 48 papers between 1980 and 2005.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2005

A Visual Interactive Framework for Formal Derivation.

Paul Agron, Leo Bachmair, Frank Nielsen

Proceedings of the Computational Science, 2005

2004

On the Combination of Congruence Closure and Completion.

Christelle Scharff, Leo Bachmair

Proceedings of the Artificial Intelligence and Symbolic Computation, 2004

2003

Abstract Congruence Closure.

Leo Bachmair, Ashish Tiwari, Laurent Vigneron

J. Autom. Reason., 2003

2001

Resolution Theorem Proving.

Leo Bachmair, Harald Ganzinger

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Congruence Closure Modulo Associativity and Commutativity.

Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, Laurent Vigneron

Proceedings of the Frontiers of Combining Systems, 2000

Rigid <i>E</i>-Unification Revisited.

Ashish Tiwari, Leo Bachmair, Harald Rueß

Proceedings of the Automated Deduction, 2000

Abstract Congruence Closure and Specializations.

Leo Bachmair, Ashish Tiwari

Proceedings of the Automated Deduction, 2000

1999

Normalization via Rewrite Closures.

Leo Bachmair, C. R. Ramakrishnan, I. V. Ramakrishnan, Ashish Tiwari

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

1998

Ordered Chaining Calculi for First-Order Theories of Transitive Relations.

Leo Bachmair, Harald Ganzinger

J. ACM, 1998

An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction.

Maxim Lifantsev, Leo Bachmair

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

Elimination of Equality via Transformation with Ordering Constraints.

Leo Bachmair, Harald Ganzinger, Andrei Voronkov

Proceedings of the Automated Deduction, 1998

Strict Basic Superposition.

Leo Bachmair, Harald Ganzinger

Proceedings of the Automated Deduction, 1998

1997

D-Bases for Polynomial Ideals over Commutative Noetherian Rings.

Leo Bachmair, Ashish Tiwari

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

Paramodulation, Superposition, and Simplification.

Leo Bachmair

Proceedings of the Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, 1997

1996

Subsumption Algorithms Based on Search Trees.

Leo Bachmair, Ta Chen, C. R. Ramakrishnan, I. V. Ramakrishnan

Proceedings of the Trees in Algebra and Programming, 1996

1995

Basic Paramodulation

Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder

Inf. Comput., September, 1995

Experiments with Associative-Commutative Discrimination Nets.

Leo Bachmair, Ta Chen, I. V. Ramakrishnan, Siva Anantharaman, Jacques Chabin

Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, 1995

1994

Rewrite-Based Equational Theorem Proving with Selection and Simplification.

Leo Bachmair, Harald Ganzinger

J. Log. Comput., 1994

Equational Inference, Canonical Proofs, and Proof Orderings.

Leo Bachmair, Nachum Dershowitz

J. ACM, 1994

Refutational Theorem Proving for Hierarchic First-Order Theories.

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Appl. Algebra Eng. Commun. Comput., 1994

Rewrite Techniques for Transitive Relations

Leo Bachmair, Harald Ganzinger

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Associative-Commutative Superposition.

Leo Bachmair, Harald Ganzinger

Proceedings of the Conditional and Typed Rewriting Systems, 4th International Workshop, 1994

Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings.

Leo Bachmair, Harald Ganzinger, Jürgen Stuber

Proceedings of the Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30, 1994

Buchberger's Algorithm: A Constraint-Based Completion Procedure.

Leo Bachmair, Harald Ganzinger

Proceedings of the Constraints in Computational Logics, First International Conference, 1994

Ordered Chaining for Total Orderings.

Leo Bachmair, Harald Ganzinger

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

Associative-Commutative Discrimination Nets.

Leo Bachmair, Ta Chen, I. V. Ramakrishnan

Proceedings of the TAPSOFT'93: Theory and Practice of Software Development, 1993

Rewrite Techniques in Theorem Proving (Abstract).

Leo Bachmair

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Set Constraints are the Monadic Class

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality.

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Proceedings of the Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, 1993

1992

Associative-Commutative Reduction Orderings.

Leo Bachmair

Inf. Process. Lett., 1992

Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria.

Leo Bachmair, Harald Ganzinger

Proceedings of the Logic Programming and Automated Reasoning, 1992

Basic Paramodulation and Superposition.

Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder

Proceedings of the Automated Deduction, 1992

Theorem Proving for Hierarchic First-Order Theories.

Leo Bachmair, Harald Ganzinger, Uwe Waldmann

Proceedings of the Algebraic and Logic Programming, 1992

1991

Perfect Model Semantics for Logic Programs with Equality.

Leo Bachmair, Harald Ganzinger

Proceedings of the Logic Programming, 1991

1990

Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract).

Leo Bachmair, Harald Ganzinger

Proceedings of the Conditional and Typed Rewriting Systems, 1990

On Restrictions of Ordered Paramodulation with Simplification.

Leo Bachmair, Harald Ganzinger

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

Completion for Rewriting Modulo a Congruence.

Leo Bachmair, Nachum Dershowitz

Theor. Comput. Sci., 1989

Proof Normalization for Resolution and Paramodulation.

Leo Bachmair

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

1988

Critical Pair Criteria for Completion.

Leo Bachmair, Nachum Dershowitz

J. Symb. Comput., 1988

Proof by Consistency in Equational Theories

Leo Bachmair

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

1987

Inference Rules for Rewrite-Based First-Order Theorem Proving

Leo Bachmair, Nachum Dershowitz

Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

A critical pair criterion for completion modulo a congruence.

Leo Bachmair, Nachum Dershowitz

Proceedings of the EUROCAL '87, 1987

1986

Orderings for Equational Proofs

Leo Bachmair, Nachum Dershowitz, Jieh Hsiang

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Critical-pair criteria for the Knuth-Bendix completion procedure.

Leo Bachmair, Nachum Dershowitz

Proceedings of the Symposium on Symbolic and Algebraic Manipulation, 1986

Commutation, Transformation, and Termination.

Leo Bachmair, Nachum Dershowitz

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

Termination Orderings for Associative-Commutative Rewriting Systems.

Leo Bachmair, David A. Plaisted

J. Symb. Comput., 1985

Associative Path Orderings.

Leo Bachmair, David A. Plaisted

Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985

1980

A simplified proof of the characterization theorem for Gröbner-bases.

Leo Bachmair, Bruno Buchberger

SIGSAM Bull., 1980