Sylvain Conchon and Sava Krstic.
Strategies for combining decision procedures.
In P. Narendran and M. Rusinowitch, editors, Proceedings of the 9th
International Conference on Tools and Algorithms for the Construction and
Analysis of Systems (Warsaw, Poland), volume 2619 of Lecture
Notes in Computer Science, pages 537-553. Springer-Verlag, April
2003.
(BibTex Entry)
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz,
and Roberto Sebastiani.
Integrating boolean and mathematical solving: Foundations, basic
algorithms and requirements.
In Proceedings of the Joint international Conference on Artificial
Intelligence, Automated Reasoning, and Symbolic Computation, volume
2385 of Lecture Notes in Artificial Intelligence. Springer,
2002.
(BibTex Entry)
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz,
and Roberto Sebastiani.
A SAT-based approach for solving formulas over boolean and linear
mathematical propositions.
In Andrei Voronkov, editor, Proceedings of the 18th International
Conference on Automated Deduction, volume 2392 of Lecture Notes
in Artificial Intelligence, pages 195-210. Springer, 2002.
(BibTex Entry)
Clark W. Barrett, David L. Dill, and Aaron Stump.
Checking satisfiability of first-order formulas by incremental
translation to SAT.
In J. C. Godskesen, editor, Proceedings of the International Conference
on Computer-Aided Verification, Lecture Notes in Computer Science,
2002.
(BibTex Entry)
Clark W. Barrett, David L. Dill, and Aaron Stump.
A
generalization of Shostak's method for combining decision
procedures.
In A. Armando, editor, Proceedings of the 4th International Workshop on
Frontiers of Combining Systems, FroCoS'2002 (Santa Margherita Ligure,
Italy), volume 2309 of Lecture Notes in Computer Science,
pages 132-147, apr 2002.
(BibTex Entry)
Leonardo de Moura and Harald Rueß.
Lemmas on demand for satisfiability solvers.
Presented at the Fifth International Symposium on the Theory and Applications
of Satisfiability Testing (SAT'02), Cincinnati, USA, May 2002.
(BibTex Entry)
Harald Ganzinger.
Shostak light.
In A. Voronkov, editor, Proceedings of the 18th International Conference
on Automated Deduction, volume 2392 of Lecture Notes in Computer
Science, pages 332-346. Springer-Verlag, jul 2002.
(BibTex Entry)
Predrag Janicic and Alan Bundy.
A general setting for flexibly combining and augmenting decision
procedures.
Journal of Automated Reasoning, 28(3):257-305, April
2002.
(BibTex Entry)
Deepak Kapur.
A rewrite rule based framework for combining decision
procedures.
In Alessandro Armando, editor, Proceedings of the 4th International
Workshop on Frontiers of Combining Systems (Santa Margherita Ligure,
Italy), volume 2309 of Lecture Notes in Computer Science,
pages 87-102. Springer, April 2002.
(BibTex Entry)
Natarajan Shankar.
Little
engines of proof.
In Lars-Henrik Eriksson and Peter A. Lindsay, editors, FME 2002: Formal
Methods - Getting IT Right, Proceedings of the International Symposium of
Formal Methods Europe (Copenhagen, Denmark), volume 2391 of
Lecture Notes in Computer Science, pages 1-20. Springer, July
2002.
(BibTex Entry)
Natarajan Shankar and Harald Rueß.
Combining
shostak theories.
In S. Tison, editor, Proceedings of the 13th International Conference on
Rewriting Techniques and Applications (Copenhagen, Denmark), volume
2378 of Lecture Notes in Computer Science, pages 1-18.
Springer, July 2002.
(BibTex Entry)
Aaron Stump, Clark W. Barrett, and David L. Dill.
CVC: a cooperating validity checker.
In J. C. Godskesen, editor, Proceedings of the International Conference
on Computer-Aided Verification, Lecture Notes in Computer Science,
2002.
(BibTex Entry)
Cesare Tinelli.
A
DPLL-based calculus for ground satisfiability modulo theories.
In Giovambattista Ianni and Sergio Flesca, editors, Proceedings of the
8th European Conference on Logics in Artificial Intelligence (Cosenza,
Italy), volume 2424 of Lecture Notes in Artificial
Intelligence. Springer, 2002.
(BibTex Entry)
Calogero Zarba.
A tableau calculus for combining non-disjoint theories.
In U. Egly and C. Fermüller, editors, Proceedings of the
International Conference on Automated Reasoning with Analytic Tableaux and
Related Methods, TABLEAUX 2002 (Copenhagen, Denmark), volume 2381 of
Lecture Notes in Computer Science, pages 315-329. Springer,
2002.
(BibTex Entry)
Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, and Natarajan
Shankar.
Ics:
Integrated canonizer and solver.
In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Proceedings
of the 13th International Conference on Computer Aided Verification (Paris,
France), volume 2102 of Lecture Notes in Computer
Science, pages 246-249. Springer-Verlag, July 2001.
(BibTex Entry)
Jürgen Giesl and Deepak Kapur.
Decidable classes of inductive theorems.
In R. Goré, A. Leitsch, and T. Nipkow, editors, Proceedings of the
First International Joint Conference on Automated Reasoning, IJCAR 2001,
(Siena, Italy), volume 2083 of Lecture Notes in Artificial
Intelligence, pages 469-484. Springer, 2001.
(BibTex Entry)
Harald Rueß and Natarajan Shankar.
Deconstructing Shostak.
In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer
Science (Boston, Massachusetts, USA), pages 19-28. IEEE Computer
Society, June 2001.
(BibTex Entry)
Calogero G. Zarba.
Combining lists with integers.
In R. Goré, A. Leitsch, and T. Nipkov, editors, International Joint
Conference on Automated Reasoning, IJCAR'01 (Short Papers), Technical
Report DII 11/01, pages 180-189. University of Siena, Italy, 2001.
(BibTex Entry)
Calogero G. Zarba.
Combining non-disjoint theories.
In R. Goré, A. Leitsch, and T. Nipkov, editors, International Joint
Conference on Automated Reasoning, IJCAR'01 (Short Papers), Technical
Report DII 11/01, pages 180-189. University of Siena, Italy, 2001.
(BibTex Entry)
Alessandro Armando and Silvio Ranise.
Termination of constraint contextual rewriting.
In H. Kirchner and Ch. Ringeissen, editors, Proceedings of the 3rd
International Workshop on Frontiers of Combining Systems, FroCoS'2000,
Nancy (France), volume 1794 of Lecture Notes in Artificial
Intelligence, pages 47-61. Springer-Verlag, March 2000.
(BibTex Entry)
Alessandro Armando, Claudio Castellini, and Enrico Giunchiglia.
SAT-based procedures for temporal reasoning.
In S. Biundo and M. Fox, editors, Proceedings of the 5th European
Conference on Planning (Durham, UK), volume 1809 of Lecture
Notes in Computer Science, pages 97-108. Springer, 2000.
(BibTex Entry)
Franz Baader and Cesare Tinelli.
Combining equational theories sharing non-collapse-free
constructors.
In H. Kirchner and Ch. Ringeissen, editors, Proceedings of the 3rd
International Workshop on Frontiers of Combining Systems, FroCoS'2000,
Nancy (France), volume 1794 of Lecture Notes in Artificial
Intelligence, pages 260-274. Springer-Verlag, March 2000.
(BibTex Entry)
Leo Bachmair and Ashish Tiwari.
Abstract congruence closure and specializations.
In D. A. McAllester, editor, Proceedings of the 17th International
Conference on Automated Deduction (Pittsburgh, PA), volume 1831 of
Lecture Notes in Artificial Intelligence, pages 64-78.
Springer, 2000.
(BibTex Entry)
Leo Bachmair, I. V. Ramakrishnan, Ashis Tiwari, and Laurent Vigneron.
Congruence closure modulo associativity and commutativity.
In H. Kirchner and Ch. Ringeissen, editors, Proceedings of the 3rd
International Workshop on Frontiers of Combining Systems, FroCoS'2000,
Nancy (France), volume 1794 of Lecture Notes in Artificial
Intelligence, pages 245-259. Springer-Verlag, March 2000.
(BibTex Entry)
Clark W. Barrett, David L. Dill, and Aaron Stump.
A framework for
cooperating decision procedures.
In D. A. McAllester, editor, Proceedings of the 17th International
Conference on Automated Deduction (Pittsburgh, PA), volume 1831 of
Lecture Notes in Artificial Intelligence, pages 79-98.
Springer, 2000.
(BibTex Entry)
Camillo Fiorentini and Silvio Ghilardi.
Path rewriting and combined word problems.
Technical Report 250-00, Department of Computer Science, Università degli
Studi di Milano, Milan, Italy, May 2000.
(BibTex Entry)
Miki Hermann and Phokion G. Kolaitis.
Unification algorithms cannot be combined in polynomial time.
Information and Computation, 162(1-2):24-42, 2000.
(BibTex Entry)
Deepak Kapur.
Rewriting, induction and decision procedures: A case study of
Presburger arithmetic.
In G. Alefeld, J. Rohn, S. Rump, and T. Yamamoto, editors, Symbolic
Algebraic Methods and Verification Methods, pages 129-144. Springer
Mathematics, 2000.
(BibTex Entry)
Deepak Kapur and Mahadevan Subramaniam.
Extending decision procedures with induction schemes.
In D. A. McAllester, editor, Proceedings of the 17th International
Conference on Automated Deduction (Pittsburgh, PA), volume 1831 of
Lecture Notes in Artificial Intelligence, pages 324-345.
Springer, 2000.
(BibTex Entry)
Stephan Kepser.
Negation in combining constraint systems.
In M. de Rijke and D. Gabbay, editors, Frontiers of Combining Systems
2, Studies in Logic and Computation, pages 177-192. Research Studies
Press/Wiley, 2000.
(BibTex Entry)
Grigore Rosu and Joseph Goguen.
On
equational Craig interpolation.
Journal of Universal Computer Science, 6(1):194-200, February
2000.
(special issue in honor of Prof. Rudeanu, edited by Christian Calude).
(BibTex Entry)
Klaus U. Schulz.
Why combined decision problems are often intractable.
In H. Kirchner and Ch. Ringeissen, editors, Proceedings of the 3rd
International Workshop on Frontiers of Combining Systems, FroCoS'2000,
Nancy (France), volume 1794 of Lecture Notes in Artificial
Intelligence, pages 217-244. Springer-Verlag, March 2000.
(BibTex Entry)
Calogero G. Zarba and Domenbico Cantone.
A tableau calculus for integrating first-order reasoning with
elementary set theory reasoning.
In R. Dyckhoff, editor, Proceedings of the International Conference on
Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 200
(St Andrew, Scotland), volume 1847 of Lecture Notes in
Artificial Intelligence, pages 143-159. Springer, 2000.
(BibTex Entry)
Predrag Janicic, Alan Bundy, and Ian Green.
A framework for the flexible integration of a class of decision
procedures into theorem provers.
In H. Ganzinger, editor, Proceedings of the 16th Conference on Automated
Deduction, CADE-16, number 1632 in Lecture Notes in Artificial
Intelligence, pages 127-141. Springer, 1999.
(BibTex Entry)
Stephan Kepser and Jörn Richts.
UniMoK: A system for combining equational unification
algorithms.
In P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th
International Conference on Rewriting Techniques and Applications (Trento,
Italy), Lecture Notes in Computer Science. Springer-Verlag, 1999.
(BibTex Entry)
Alessandro Armando and Silvio Ranise.
Constraint contextual rewriting.
In R. Caferra and G. Salzer, editors, Proceedings of the 2nd
International Workshop on First Order Theorem Proving, FTP'98, Vienna
(Austria), pages 65-75, November 1998.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
Combination of constraint solvers for free and quasi-free
structures.
Theoretical Computer Science, 192:107-161, 1998.
(BibTex Entry)
Peter Baumgartner.
Theory Reasoning in Connection Calculi, volume 1527 of
Lecture Notes in Artificial Intelligence.
Springer Verlag, 1998.
(BibTex Entry)
Peter Baumgartner and Uwe Petermann.
Chapter II.6: Theory Reasoning.
In W. Bibel and P. H. Schmitt, editors, Automated Deduction. A Basis for
Applications, volume I: Foundations. Calculi and Refinements, pages
191-224. Kluwer Academic Publishers, 1998.
(BibTex Entry)
Nikolaj S. Bjørner.
Integrating Decision Procedures for Temporal Verification.
PhD dissertation, Department of Computer Science, Stanford University,
Stanford, CA, November 1998.
(BibTex Entry)
David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe.
Extended static checking.
Research Report #159, Compaq Systems Research Center, Palo Alto, USA, December
1998.
(BibTex Entry)
Bernhard Gramlich.
Modular aspects of rewrite-based specifications.
In F. Parisi-Presicce, editor, Recent Trends in Algebraic Development
Techniques, 12th International Workshop, WADT 97, (Tarquinia, Italy),
Selected Papers, volume 1376 of Lecture Notes in Computer
Science, pages 253-268. Springer-Verlag, 1998.
(BibTex Entry)
Stephan Kepser.
Combination of Constraint Systems.
PhD dissertation, Centre for Information and Language Processing, University
of Munich, Munich, Germany, 1998.
(BibTex Entry)
K. Rustan M. Leino and Greg Nelson.
An extended static checker for Modula-3.
In Kai Koskimies, editor, Proceedings of the 7th International Conference
on Compiler Construction, CC'98, volume 1383 of Lecture Notes
in Computer Science, pages 302-305. Springer, April 1998.
(BibTex Entry)
Frank Wolter.
Fusions of modal logics revisited.
In M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, editors,
Advances in Modal Logic. CSLI, Stanford, CA, 1998.
(BibTex Entry)
Farid Ajili and Claude Kirchner.
A modular framework for the combination of unification and built-in
constraints.
In L. Naish, editor, Proceedings of the 14th International Conference on
Logic Programming, pages 331-345. MIT Press, July 1997.
(BibTex Entry)
Nikolaj S. Bjørner, Mark. E. Stickel, and Tomás E. Uribe.
A
practical integration of first-order reasoning and decision
procedures.
In W. McCune, editor, Proceedings of the 14th International Conference on
Automated Deduction, CADE-14 (Townsville, Australia), volume 1249 of
Lecture Notes in Artificial Intelligence, pages 101-115,
1997.
(BibTex Entry)
Deepak Kapur.
Shostak's congruence closure as completion.
In H. Comon, editor, Proceedings of the 8th International Conference on
Rewriting Techniques and Applications, volume 1232 of Lecture
Notes in Computer Science. Springer-Verlag, 1997.
(BibTex Entry)
Michael R. Lowry and Jeffrey Van Baalen.
META-AMPHION: Synthesis of efficient domain-specific program
synthesis system.
Automated Software Engineering, 4(2):199-241, April 1997.
(BibTex Entry)
Uwe Petermann.
Building-in hybrid theories.
In M. P. Bonacina and U. Furbach, editors, Proceedings of the
International Workshop on First-Order Theorem Proving, FTP'97,
RISC-Linz Report Series No. 97-50, pages 108-112. Johannes Kepler
Universität, Linz (Austria), October 1997.
(BibTex Entry)
Steven Roach.
TOPS: Theory Operationalization for Program Synthesis.
PhD dissertation, Department of Computer Science, University of Wyoming,
August 1997.
(BibTex Entry)
Klaus U. Schulz.
A criterion for intractability of E-unification with free function
symbols and its relevance for combination of unification algorithms.
In H. Comon, editor, Proceedings of the 8th International Conference on
Rewriting Techniques and Applications, volume 1232 of Lecture
Notes in Computer Science, pages 284-298. Springer-Verlag, 1997.
(BibTex Entry)
Farid Ajili and Claude Kirchner.
Combining unification and built-in constraints.
In K.U. Schulz and S. Kepser, editors, Proceedings of the 10th
International Workshop on Unification, UNIF'96. CIS-Report 96-9,
CIS, Universität München, June 1996.
(extended abstract).
(BibTex Entry)
Franz Baader and Werner Nutt.
Combination problems for commutative/monoidal theories: How algebra
can help in equational reasoning.
Journal of Applicable Algebra in Engineering, Communication and
Computing, 7(4):309-337, 1996.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
Unification in the union of disjoint equational theories: Combining
decision procedures.
Journal of Symbolic Computation, 21(2):211-243, February
1996.
(BibTex Entry)
Franz Baader and Cesare Tinelli.
A new approach for combining decision procedures for the word problem,
and its connection to the Nelson-Oppen combination method.
Technical Report 96-01, LuFG Theoretical Computer Science, RWTH-Aachen,
Germany, 1996.
(BibTex Entry)
Clark W. Barrett, David L. Dill, and Jeremy R. Levitt.
Validity checking
for combinations of theories with equality.
In M. K. Srivas and A. Camilleri, editors, Proceedings of the First
International Conference on Formal Methods in Computer-Aided Design (Palo
Alto, CA), volume 1166 of Lecture Notes in Computer
Science, pages 187-201. Springer, 1996.
(BibTex Entry)
David Basin, Sean Matthews, and Luca Vigano.
A topography of labelled modal logics.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 75-92. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Bernhard Beckert and Reiner Hähnle.
Deduction by combining semantic tableaux and integer
programming.
In H. Kleine Büning, editor, Proceedings of the Annual Conference of
the European Association for Computer Science Logic (CSL'95), Paderborn
(Germany), volume 1092 of Lecture Notes in Computer
Science, pages 52-63. Springer, 1996.
(BibTex Entry)
Bernhard Beckert and Christian Pape.
Incremental theory reasoning methods for semantic
tableaux.
In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors,
Proceedings of the 5th Workshop on Theorem Proving with Analytic
Tableaux and Related Methods, TABLEAUX'92 Palermo, (Italy), volume
1071 of Lecture Notes in Computer Science, pages 93-109.
Springer, 1996.
(BibTex Entry)
Alexandre Boudet, Evelyne Contejean, and Claude Marché.
AC-complete unification and its application to theorem
proving.
In H. Ganzinger, editor, Proceedings of the 7th International Conference
on Rewriting Techniques and Applications (RTA-96), volume 1103 of
Lecture Notes in Computer Science, pages 18-32.
Springer-Verlag, July 1996.
(BibTex Entry)
Bruno Buchberger.
Symbolic computation: Computer algebra and logic.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 193-220. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Jacques Calmet and Karsten Homann.
Classification of communication and cooperation mechanisms for logical
and symbolic computation systems.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 221-234. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Xiao Jun Chen.
Model checking ACTL constrained processes.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 377-397. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
John N. Crossley, Luis Mandel, and Martin Wirsing.
First-order constrained lambda calculus.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 339-356. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
David Cyrluk, Patrick Lincoln, and Natarajan Shankar.
On
Shostak's decision procedure for combinations of theories.
In M. A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th
International Conference on Automated Deduction, (New Brunswick, NJ),
volume 1104 of Lecture Notes in Artificial Intelligence, pages
463-477. Springer-Verlag, 1996.
(BibTex Entry)
Bernd I. Dahn and Andreas Wolf.
Natural language representation and combination of automatically
generated proofs.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 175-192. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Luis Fariñas del Cerro and Andreas Herzig.
Combining classical and intuitionistic logic, or: Intuitionistic
implication as a conditional.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 93-102. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Enrico Denti, Antonio Natali, Andrea Omicini, and Marco Venuti.
Logic tuple spaces for the coordination of heterogeneous
agents.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 235-248. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Eric Domenjoud.
Undecidability of the word problem in the union of theories sharing
constructors.
In K.U. Schulz and S. Kepser, editors, Proceedings of the 10th
International Workshop on Unification, UNIF'96. CIS-Report 96-9,
CIS, Universität München, June 1996.
(extended abstract).
(BibTex Entry)
Agostino Dovier, Alberto Policriti, and Gianfranco Rossi.
Integrating lists, multisets, and sets in a logic programming
framework.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 303-320. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Steven Eker.
Fast matching in combinations of regular equational
theories.
In J. Meseguer, editor, Proceedings of First International Workshop on
Rewriting Logic and its Applications, (Pacific Grove, CA), Electronic
Notes in Theoretical Computer Science. Elsevier Science B.V., September
1996.
(BibTex Entry)
Kit Fine and Gerhard Schurz.
Transfer theorems for stratified modal logics.
In J. Copeland, editor, Logic and Reality: Essays in Pure and Applied
Logic. In Memory of Arthur Prior, pages 169-213. Oxford
University Press, 1996.
(BibTex Entry)
Dov M. Gabbay.
Fibred semantics and the weaving of logics. Part 1. Modal and
intuitionistic logics.
The Journal of Symbolic Logic, 61(4):1057-1120, December 1996.
(BibTex Entry)
Dov M. Gabbay.
An overview of fibred semantics and the combination of logics.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 1-56. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Fausto Giunchiglia, Paolo Pecchiari, and Carolyn Talcott.
Reasoning theories - towards an architecture for open mechanized
reasoning systems.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 157-174. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Naji Habra and Baudouin Le Charlier.
Unified relational framework for programming paradigms
combination.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 357-376. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Miki Hermann and Phokion G. Kolaitis.
Unification algorithms cannot be combined in polynomial time.
In M. A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th
International Conference on Automated Deduction, (New Brunswick, NJ),
volume 1104 of Lecture Notes in Artificial Intelligence.
Springer-Verlag, 1996.
(BibTex Entry)
Stephan Kepser and Klaus U. Schulz.
Combination of constraint systems II: Rational amalgamation.
In E. C. Freuder, editor, Proceedings of the 2nd International Conference
on Principles and Practice of Constraint Programming, Cambridge, MA,
USA, volume 1118 of Lecture Notes in Computer Science,
pages 282-296. Springer-Verlag, August 1996.
(BibTex Entry)
Evelina Lamma, Michela Milano, and Paola Mello.
Combining constraint solvers in a meta clp architecture.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 267-284. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Christopher Landauer and Kirstie L. Bellman.
Integration systems and interaction spaces.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 249-266. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Fred Mesnard, Sebastien Hoarau, and Alexandra Maillard.
CLP(X) for proving program properties.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 321-338. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Eric Monfroy.
An environment for designing/executing constraint solver
collaborations.
Technical Report 96-R-044, Centre de Recherche en Informatique de Nancy,
1996.
(BibTex Entry)
Eric Monfroy and Christophe Ringeissen.
Domain-independent constraint solver extension.
Technical Report 96-R-043, Centre de Recherche en Informatique de Nancy,
1996.
(BibTex Entry)
Eric Monfroy, Michael Rusinowitch, and Rene Schott.
Implementing non-linear constraints with cooperative
solvers.
In K. M. George, J. H. Carroll, D. Oppenheim, and J. Hightower, editors,
Proceedings of the ACM Symposium on Applied Computing, SAC '96,
pages 63-72. ACM, February 1996.
Also available as INRIA-Research Report RR2747.
(BibTex Entry)
Uwe Petermann.
Multi-modal reasoning as reasoning in hybrid theories.
In Proceedings of the 5th Workshop on Theorem Proving with Analytic
Tableaux and Related Methods, TABLEAUX'96 Palermo, (Italy), Lecture
Notes in Computer Science. Springer, 1996.
(BibTex Entry)
Jörn Richts.
Optimization for combining unification algorithms.
In K.U. Schulz and S. Kepser, editors, Proceedings of the 10th
International Workshop on Unification, UNIF'96. CIS-Report 96-9,
CIS, Universität München, June 1996.
(extended abstract).
(BibTex Entry)
Christophe Ringeissen.
Combining decision algorithms for matching in the union of disjoint
equational theories.
Information and Computation, 126(2):144-160, May 1996.
(BibTex Entry)
Christophe Ringeissen.
Cooperation of decision procedures for the satisfiability
problem.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 121-140. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Alessandra Russo.
Generalising propositional modal logic using labelled deductive
systems.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 57-74. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
John Slaney and Timothy J. Surendonk.
Combining finite model generation with theorem proving: Problems and
prospects.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 141-156. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Frieder Stolzenburg.
Membership-constraints and complexity in logic programming with
sets.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop, Munich (Germany),
Applied Logic, pages 285-302. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Cesare Tinelli and Mehdi T. Harandi.
Constraint logic programming over unions of constraint theories.
In E. C. Freuder, editor, Proceedings of the 2nd International Conference
on Principles and Practice of Constraint Programming (Cambridge, MA,
USA), volume 1118 of Lecture Notes in Computer Science,
pages 436-450. Springer-Verlag, August 1996.
(BibTex Entry)
Cesare Tinelli and Mehdi T. Harandi.
A new correctness proof of the Nelson--Oppen combination
procedure.
In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems:
Proceedings of the 1st International Workshop (Munich, Germany),
Applied Logic, pages 103-120. Kluwer Academic Publishers, March 1996.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
Combination techniques and decision problems for
disunification.
Theoretical Computer Science, 142:229-255, 1995.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
On the combination of symbolic constraints, solution domains, and
constraint solvers.
In Proceedings of the First International Conference on Principles and
Practice of Constraint Programming, Cassis (France), volume 976 of
Lecture Notes in Artificial Intelligence. Springer-Verlag,
September 1995.
(BibTex Entry)
Peter Baumgartner and Frieder Stolzenburg.
Constraint model elimination and a PTTP-implementation.
In P. Baumgartner, R. Hähnle, and J. Posegga, editors, Proceedings of
the 4th International Workshop on Theorem Proving with Analytic Tableaux and
Related Methods, TABLEAUX'95 (St. Goar, Germany), volume 918 of
Lecture Notes in Artificial Intelligence, pages 201-216.
Springer Verlag, 1995.
(BibTex Entry)
Henri Beringer and Bruno De Backer.
Combinatorial problem solving in constraint logic programming with
cooperating solvers.
In C. Beierle and L. Plümer, editors, Logic Programming: Formal
Methods and Practical Applications, Studies in Computer Science and
Artificial Intelligence, chapter 8, pages 245-272. Elsevier, 1995.
(BibTex Entry)
Richard J. Boulton.
Combining decision procedures in the HOL system.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings
of the 8th International Workshop on Higher Order Logic Theorem Proving and
Its Applications (Aspen Grove, UT, USA), volume 971 of Lecture
Notes in Computer Science, pages 75-89. Springer-Verlag, September
1995.
(BibTex Entry)
Hubert Comon.
Constraints in term algebras.
In Andreas Podelski, editor, Constraint Programming: Basics and
Trends, volume 910 of Lecture Notes in Computer Science.
Springer-Verlag, 1995.
(Châtillon-sur-Seine Spring School, France, May 1994).
(BibTex Entry)
Andrea Formisano and Alberto Policriti.
T-resolution: Refinements and model elimination.
Technical Report UDMI/32/12/95, Dipartimento di Matematica e Informatica,
Università di Udine, Udine, Italy, 1995.
(BibTex Entry)
Hélène Kirchner.
On the use of constraints in automated deduction.
In Andreas Podelski, editor, Constraint Programming: Basics and
Trends, volume 910 of Lecture Notes in Computer Science.
Springer-Verlag, 1995.
(Châtillon-sur-Seine Spring School, France, May 1994).
(BibTex Entry)
Philippe Marti and Michel Rueher.
A distributed cooperating constraints solving system.
International Journal of Artificial Intelligence Tools,
4(1-2):93-113, 1995.
(BibTex Entry)
P. Baumgartner, J.-J. Bürckert, H. Comon, A. M. Frisch, U. Furbach, Murray,
U. Petermann, and M. E. Stickel.
Theory Reasoning in Automated
Deduction.
Research Report 8-94, Universität Koblenz-Landau, 1994.
Fachberichte Informatik.
(BibTex Entry)
D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas.
Effective
theorem proving for hardware verification.
In Proceedings of the 2nd International Conference on Theorem Provers in
Circuit Design, Theory, Practice, and Experience (Bad Herrenalb,
Germany), volume 901 of Lecture Notes in Computer
Science, pages 203-222. Springer-Verlag, 1994.
(BibTex Entry)
Eric Domenjoud, Francis Klay, and Christophe Ringeissen.
Combination techniques for non-disjoint equational
theories.
In A. Bundy, editor, Proceedings of the 12th International Conference on
Automated Deduction, Nancy (France), volume 814 of Lecture Notes
in Artificial Intelligence, pages 267-281. Springer-Verlag, 1994.
(BibTex Entry)
Ulrich Furbach.
Theory reasoning in first order calculi.
In K. von Luck and H. Marburger, editors, Proceedings of the Third
Workshop on Information Systems and Artificial Intelligence, volume
777 of Lecture Notes in Computer Science. Springer-Verlag,
February 1994.
(BibTex Entry)
Bernhard Gramlich.
Generalized sufficient conditions for modular termination of
rewriting.
Applicable Algebra in Engineering, Communication and Computing,
5:131-158, 1994.
(BibTex Entry)
Philippe Marti and Michel Rueher.
A cooperative scheme for solving constraints over the reals.
In H. Hong, editor, First International Symposium on Parallel Symbolic
Computation, PASCO'94, (Hagenberg slash Linz, Austria), volume 5 of
Lecture notes series in computing, pages 284-293, Singapore;
Philadelphia, PA, USA; River Edge, NJ, USA, 1994. World Scientific Publishing
Co.
(BibTex Entry)
Aart Middeldorp.
Completeness of combinations of conditional constructor
systems.
Journal of Symbolic Computation, 17(1):3-21, January 1994.
(BibTex Entry)
Christian Prehofer.
On modularity in term rewriting and narrowing.
In J.-P. Jouannaud, editor, Proceedings of the First International
Conference on Constraints in Computational Logics, Munich (Germany),
volume 845 of Lecture Notes in Computer Science.
Springer-Verlag, 1994.
(BibTex Entry)
Christophe Ringeissen.
Combination of matching algorithms.
In P. Enjalbert, E. W. Mayr, and K. W. Wagner, editors, Proceedings 11th
Annual Symposium on Theoretical Aspects of Computer Science, Caen
(France), volume 775 of Lecture Notes in Artificial
Intelligence, pages 187-198. Springer-Verlag, February 1994.
(BibTex Entry)
Richard B. Scherl.
Equality and constrained resolution.
In C. MacNish, D. Pearce, and L. Moniz Pereira, editors, Proceedings of
the Joint European Workshop on Logics in AI (JELIA'94), volume 838
of Lecture Notes in Artificial Intelligence, pages 167-181.
Springer-Verlag, September 1994.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
Combination techniques and decision problems for
disunification.
In C. Kirchner, editor, Proceedings of the 5th International Conference
on Rewriting Techniques and Applications, volume 690 of Lecture
Notes in Computer Science, pages 301-315. Springer-Verlag, 1993.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
General A- and AX-Unification via optimized combination
procedures.
In Proceedings of the Second International Workshop on Word Equations and
Related Topics (Rouen, France), volume 677 of Lecture Notes in
Artificial Intelligence, pages 23-42. Springer-Verlag, 1993.
(BibTex Entry)
Hubert Comon.
Constraints in term algebras (A short survey).
In M. Nivat, C. Rattay, T. Rus, and G. Scollo, editors, Proceedings of
Algebraic Methodology and Software Technology, pages 145-152,
Enschede, Netherlands, June 1993.
(BibTex Entry)
Razvan Diaconescu, Joseph Goguen, and Petros Stefaneas.
Logical
support for modularization.
In G. Huet and G. Plotkin, editors, Logical Environments, pages
83-130. Cambridge Press, 1993.
(BibTex Entry)
Claude Kirchner, Hélène Kirchner, and Marian Vittek.
Implementing computational systems with constraints.
In P. van Hentenryck and V. Saraswat, editors, Proceedings of the First
Workshop on Principles and Practice of Constraints Programming,
Newport, Rhode Island, April 1993. MIT Press.
(BibTex Entry)
Aart Middeldorp and Yoshihito Toyama.
Completeness of combinations of constructor systems.
Journal of Symbolic Computation, 15(3):331-348, March 1993.
(BibTex Entry)
Christophe Ringeissen.
Combinaison de Résolutions de Contraines.
Thèse de Doctorat d' Université, Université de Nancy 1,
Nancy, France, December 1993.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
Unification in the union of disjoint equational theories: Combining
decision procedures.
In D. Kapur, editor, Proceedings of the 11th International Conference on
Automated Deduction, volume 607 of Lecture Notes in Artificial
Intelligence, pages 50-65. Springer-Verlag, 1992.
(BibTex Entry)
Peter Baumgartner.
A model elimination calculus with built-in theories.
In H. B. Ohlbach, editor, Proceedings of the 6th German Conference on
Artificial Intelligence, GWAI-92, volume 671 of Lecture Notes in
Computer Science, pages 30-42. Springer-Verlag, September 1992.
(BibTex Entry)
Peter Baumgartner.
An ordered theory resolution calculus.
In A. Voronkov, editor, Proceedings of the 1st International Conference
on Logic Programming and Automated Reasoning, volume 624 of
Lecture Notes in Artificial Intelligence, pages 119-130.
Springer Verlag, July 1992.
(BibTex Entry)
Peter Baumgartner, Ulrich Furbach, and Uwe Petermann.
A unified approach to theory reasoning.
Research Report 15-92, Universität Koblenz-Landau, Koblenz, Germany, 1992.
Fachberichte Informatik.
(BibTex Entry)
Alexandre Boudet.
Unification in order-sorted algebras with overloading.
In D. Kapur, editor, Proceedings of the 11th International Conference on
Automated Deduction (Saratoga Springs, NY), volume 607.
Springer-Verlag, June 1992.
(BibTex Entry)
Alan M. Frisch and Anthony G. Cohn.
An abstract view of sorted unification.
In D. Kapur, editor, Proceedings of the 11th International Conference on
Automated Deduction, volume 607 of Lecture Notes in Artificial
Intelligence, pages 178-192, Saratoga Springs, New York, USA, June
1992. Springer-Verlag.
(BibTex Entry)
Bernhard Gramlich.
Generalized sufficient conditions for modular termination of
rewriting.
In H. Kirchner and G. Levi, editors, Proceedings of the 3rd International
Conference on Algebraic and Logic Programming, Pisa, Italy, volume 632
of Lecture Notes in Computer Science, pages 53-68.
Springer-Verlag, September 1992.
(BibTex Entry)
C. David Page Jr. and Alan Frisch.
Generalization and learnability: A study of constrained
atoms.
In S. H. Muggleton, editor, Inductive Logic Programming, pages
29-61. Academic Press, London, 1992.
(BibTex Entry)
Hélène Kirchner and Christophe Ringeissen.
Combining unification problems with constraint solving in finite
algebras.
Technical Report 91-R-106, Centre de Recherche en Informatique de Nancy,
1992.
(BibTex Entry)
Masahito Kurihara and Azuma Ohuchi.
Modularity of simple termination of term rewriting systems with shared
constructors.
Theoretical Computer Science, 103(2):273-282, 1992.
(BibTex Entry)
Uwe Petermann.
Proving completeness of connection and other first-order calculi with
built-in theories (extended abstract).
In B. Fronhöfer, R. Hähnle, and T. Káufl, editors,
Proceedings of the Workshop on Theorem Proving with Analytic Tableaux
and Related Methods, TABLEAUX'92, Karlsruhe (Germany), pages 64-66,
1992.
(BibTex Entry)
Christophe Ringeissen.
Unification in a combination of equational theories with shared
constants and its application to primal algebras.
In A. Voronkov, editor, Proceedings of the 1st International Conference
on Logic Programming and Automated Reasoning, volume 624 of
Lecture Notes in Artificial Intelligence, pages 261-272.
Springer-Verlag, 1992.
(BibTex Entry)
Franz Baader and Klaus U. Schulz.
Unification in the union of disjoint equational theories: Combining
decision procedures.
Technical Report RR-91-33, DFKI, November 1991.
(BibTex Entry)
Jeffrey Van Baalen.
The completeness of DRAT, a technique for automatic design of
satisfiability procedures..
In J. Allen, R. Fikes, and E. Sandewall, editors, Proceedings of the 2nd
International Conference on Principles of Knowledge Representation and
Reasoning, Cambridge, MA, USA, pages 514-525. Morgan Kaufmann
Publishers, April 1991.
(BibTex Entry)
H. Comon, H. Ganzinger, C. Kirchner, H. Kirchner, J. L. Lassez, and G. Smolka.
Theorem proving and logic programming with constraints.
Technical Report 24, Schloss Dagstuhl, October 1991.
(BibTex Entry)
Alan M. Frisch.
The substitutional framework for sorted deduction: Fundamental results
on hybrid reasoning.
Artificial Intelligence, 49(1-3):161-198, 1991.
(BibTex Entry)
Alan M. Frisch and Richard B. Scherl.
A general framework for modal deduction.
In J. Allen, R. Fikes, and E. Sandewall, editors, Proceedings of the 2nd
International Conference on Principles of Knowledge Representation and
Reasoning, pages 196-207. Morgan Kaufmann Publishers, April 1991.
(BibTex Entry)
C. David Page Jr. and Alan M. Frisch.
Generalizing atoms in constraint logic.
In J. Allen, R. Fikes, and E. Sandewall, editors, Proceedings of the 2nd
International Conference on Principles of Knowledge Representation and
Reasoning, pages 429-440. Morgan Kaufmann Publishers, April 1991.
(BibTex Entry)
Aart Middeldorp and Yoshihito Toyama.
Completeness of combinations of constructors systems.
In R. V. Book, editor, Proceedings of the 4th International Conference on
Rewriting Techniques and Applications, Como (Italy), volume 488 of
Lecture Notes in Computer Science. Springer-Verlag, 1991.
(BibTex Entry)
Alexandre Boudet.
Unification dans les mélange de théories
équationelles.
Thèse de Doctorat d' Université, Université de
Paris- Sud, Orsay, France, February 1990.
(BibTex Entry)
Alexandre Boudet.
Unification in a combination of equational theories: An efficient
algorithm.
In M. E. Stickel, editor, Proceedings of the 10th International
Conference on Automated Deduction, volume 449 of Lecture Notes
in Artificial Intelligence. Springer-Verlag, 1990.
(BibTex Entry)
Alexandre Boudet, Evelyne Contejean, and Hervé Devie.
A new AC unification algorithm with an algorithm for solving
diophantine equations.
In Proceedings of the 5th Annual Symposium on Logic in Computer
Science, pages 289-299. IEEE Computer Society, June 1990.
(BibTex Entry)
Alan M. Frisch and Richard B. Scherl.
A constraint logic approach to modal deduction.
In J. van Eijck, editor, Proceedings of the Joint European Workshop on
Logics in AI (JELIA'90), volume 478 of Lecture Notes in
Artificial Intelligence, pages 234-250. Springer-Verlag, September
1990.
(BibTex Entry)
Thomas Käufl and Nicolas Zabel.
Cooperation of decision procedures in a tableau-based theorem
prover.
Revue d'Intelligence Artificielle, 4(3):99-126, 1990.
(BibTex Entry)
Claude Kirchner, Hélène Kirchner, and Michael Rusinowitch.
Deduction with symbolic constraints.
Revue Française d'Intelligence Artificielle, 4(3):9-52, 1990.
Special issue on Automatic Deduction.
(BibTex Entry)
Uwe Petermann.
Towards a connection procedure with built in theories.
In J. van Eijck, editor, Proceedings of the Joint European Workshop on
Logics in AI, JELIA'90, volume 478 of Lecture Notes in
Artificial Intelligence, pages 444-543. Springer-Verlag, September
1990.
(BibTex Entry)
Manfred Schmidt-Schauß.
Unification in a combination of arbitrary disjoint equational
theories.
In C. Kirchner, editor, Unification, pages 217-266. Academic
Press, London, 1990.
(BibTex Entry)
Alexandre Boudet.
A new combination technique for AC unification.
In H.-J. Bürckert and W. Nutt, editors, Extended Abstracts of the 3rd
International Workshop on Unification, SEKI-Report SR-89-17, pages
22-27. Fachbereich Informatik, Universität Kaiserslautern, June 1989.
(BibTex Entry)
Claude Kirchner.
From unification in combination of equational theories to a new
AC-unification algorithm.
In H. Ait-Kaci and M. Nivat, editors, Resolutions of Equations in
Algebraic Structures: Rewriting Techniques, volume 2, pages 171-210.
Academic Press, New York, 1989.
(BibTex Entry)
Claude Kirchner and Hélène Kirchner.
Constrained equational reasoning.
In Proceedings of the ACM-SIGSAM 1989 International Symposium on
Symbolic and Algebraic Computation, Portland (Oregon), pages
382-389. ACM Press, July 1989.
Report CRIN 89-R-220.
(BibTex Entry)
Claude Kirchner and Hélène Kirchner.
Constrained equational reasoning for completion.
In Hans-Jürgen Bürckert and Werner Nutt, editors, Extended
Abstracts of the Third International Workshop on Unification,
SEKI-Report SR-89-17, pages 160-171, Lambrecht, FRG, June 1989. Fachbereich
Informatik, Universität Kaiserslautern.
(BibTex Entry)
Aart Middeldorp and Yoshihito Toyama.
Modular aspects of properties of term rewriting systems related to
normal forms.
In N. Dershowitz, editor, Proceedings of the 3rd International Conference
on Rewriting Techniques and Applications, Chapel Hill (N.C., USA),
volume 335 of Lecture Notes in Computer Science, pages 263-277.
Springer-Verlag, April 1989.
(BibTex Entry)
Tobias Nipkow.
Combining matching algorithms: The regular case.
In N. Dershowitz, editor, Proceedings of the 3rd International Conference
on Rewriting Techniques and Applications, Chapel Hill (N.C., USA),
volume 335 of Lecture Notes in Computer Science, pages 343-358.
Springer-Verlag, April 1989.
(BibTex Entry)
Manfred Schmidt-Schauß.
Unification in a combination of arbitrary disjoint equational
theories.
Journal of Symbolic Computation, 8(1-2):51-100, July/August
1989.
Special issue on unification. Part II.
(BibTex Entry)
Yoshihito Toyama, Jan W. Klop, and Hendrik P. Barendregt.
Termination for the direct sum of left-linear term rewriting
systems.
In N. Dershowitz, editor, Proceedings of the 3rd International Conference
on Rewriting Techniques and Applications, Chapel Hill (N.C., USA),
volume 335 of Lecture Notes in Computer Science, pages 477-491.
Springer-Verlag, April 1989.
(BibTex Entry)
Alexandre Boudet, Jean-Pierre Jouannaud, and Manfred Schmidt-Schauß.
Unification in free extensions of Boolean rings and = Abelian
groups.
In Proceedings of the 3rd Annual Symposium on Logic in Computer
Science, pages 121-130. IEEE Computer Society, July 1988.
(BibTex Entry)
Manfred Schmidt-Schauß.
Unification in a combination of arbitrary disjoint equational
theories.
In Proceedings of the 9th International Conference on Automated
Deduction, volume 310 of Lecture Notes in Computer
Science, pages 378-396. Springer-Verlag, 1988.
(BibTex Entry)
Harald Ganzinger and Robert Giegerich.
A note on termination in combinations of heterogeneous term rewriting
systems.
Bulletin of the European Association of Theoretical Computer
Science, 31:22-28, 1987.
(BibTex Entry)
Alexander Herold.
Combination of Unification Algorithms in Equational Theories.
PhD thesis, Fachbereich Informatik, Universität Kaiserslautern, Germany,
1987.
(BibTex Entry)
Neil V. Murray and Erik Rosenthal.
Theory links: Applications to automated theorem proving.
Journal of Symbolic Computation, 4(2):173-190, October 1987.
(BibTex Entry)
Yoshihito Toyama.
Counterexamples to termination for the direct sum of term rewriting
systems.
Information Processing Letters, 25:141-143, 1987.
(BibTex Entry)
Katherine Yelick.
Unification in combinations of collapse-free regular theories.
Journal of Symbolic Computation, 3(1-2):153-182, April 1987.
(BibTex Entry)
Alexander Herold.
Combination of unification algorithms.
In J. Siekmann, editor, Proceedings 8th International Conference on
Automated Deduction, Oxford (UK), volume 230 of Lecture Notes in
Artificial Intelligence, pages 450-469. Springer-Verlag, 1986.
(BibTex Entry)
Erik Tidén.
First-Order Unification in Combinations of Equational
Theories.
PhD dissertation, The Royal Institute of Technology, Stockholm, 1986.
(BibTex Entry)
Erik Tidén.
Unification in combinations of collapse-free theories with disjoint
sets of function symbols.
In J. Siekmann, editor, Proceedings 8th International Conference on
Automated Deduction, Oxford (UK), volume 230 of Lecture Notes in
Artificial Intelligence, pages 431-449. Springer-Verlag, 1986.
(BibTex Entry)
Katherine Yelick.
Combining unification algorithms for confined regular equational
theories.
In J.-P. Jouannaud, editor, Proceedings of the 1st International
Conference on Rewriting Techniques and Applications (Dijon, France),
volume 202 of Lecture Notes in Computer Science, pages 365-300.
Springer-Verlag, May 1985.
(BibTex Entry)
François Fages.
Associative-commutative unification.
In Proceedings 7th International Conference on Automated
Deduction, volume 170 of Lecture Notes in Artificial
Intelligence, pages 194-208. Springer-Verlag, 1984.
(BibTex Entry)
Greg Nelson.
Combining satisfiability procedures by equality-sharing.
In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving:
After 25 Years, volume 29 of Contemporary Mathematics,
pages 201-211. American Mathematical Society, Providence, RI, 1984.
(BibTex Entry)
Leo Bachmair.
The Nelson--Oppen method for combining special theorem provers:
Implementation and application to program verification.
Diploma thesis, Johannes Kepler University, Linz, Austria, 1982.
Also: RISC-Linz Technical Report 82-17.
(BibTex Entry)
Greg Nelson and Derek C. Oppen.
Simplification by cooperating decision procedures.
ACM Trans. on Programming Languages and Systems, 1(2):245-257,
October 1979.
(BibTex Entry)
Gordon Plotkin.
Building in equational theories.
In B. Meltzer and D. Michie, editors, Machine Intelligence,
volume 7, pages 73-90, Edinburgh, Scotland, 1972. Edinburgh University
Press.
(BibTex Entry)