Franz Baader and Klaus U. Schulz.
Unification in the Union of Disjoint Equational Theories: Combining
Decision Procedures.
Research report, Center for Language and Information Processing (CIS),
Wagmüllerstr. 23, D-80538 Munich, Germany, 1993.
This is the most recent version of a paper with the same title that was
presented at CADE'92, containing some new results. Submitted for publication.
Full
paper Abstract
Klaus U. Schulz.
Word Unification and Transformation of Generalized Equations.
J. of Automated Reasoning, 11:149-184, 1993.
Full
paper Abstract
Philipp Hanschke and Jörg Würtz.
Satisfiability of the smallest binary program.
Information Processing Letters, 45(5):237-241, April 1993.
Full
paper Abstract
Joachim Niehren and Andreas Podelski.
Feature Automata and Recognizable Sets of Feature Trees.
In Marie-Claude Gaudel and Jean-Pierre Jouannaud, editors, TAPSOFT 93:
Theory and Practice of Software Development, Lecture Notes in Computer
Science, vol. 668, pages 356-375, Orsay, France, 13-16 April 1993.
Springer-Verlag.
Full
paper Abstract
Joachim Niehren, Andreas Podelski, and Ralf Treinen.
Equational and Membership Constraints for Infinite Trees.
In Claude Kirchner, editor, 5th International Conference on Rewriting
Techniques and Applications, Lecture Notes in Computer Science, vol. 690,
pages 106-120, Montreal, Canada, June 1993. Springer-Verlag.
Extended version: DFKI Research Report RR-93-14.
Full
paper Abstract
Gert Smolka.
Residuation and Guarded Rules for Constraint Logic Programming.
In Frédéric Benhamou and Alain Colmerauer, editors, Constraint Logic
Programming: Selected Research, chapter 22, pages 405-419. The MIT
Press, Cambridge, Mass., 1993.
Previous version as DFKI Research Report RR-91-13.
Full paper Abstract
Ralf Treinen.
Feature Constraints with First-Class Features.
In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical
Foundations of Computer Science, Lecture Notes in Artificial
Intelligence, vol. 711, pages 734-743, Gdansk, Poland, 30 August-3
September 1993. Springer-Verlag.
Full
paper Abstract
R. Curien.
Second Order E-Matching as a Tool for Automated Theorem Proving.
In Proceedings of 6th Portugese Conference on Artificial Intelligence,
volume 727 of Lecture Notes in Artificial Intelligence, pages
242-257, Porto (Portugal), 1993.
E. Domenjoud and F. Klay.
Shallow AC theories.
In F. Orejas, editor, Proceedings of 2nd CCL Workshop, La Escala
(Spain), September 1993.
E. Domenjoud, F. Klay, and Ch. Ringeissen.
Combination of Unification Algorithms for Non-Disjoint Equational
Theories.
In Proceedings of 7th International Workshop on Unification, UNIF'93,
Boston (MA, USA), 1993.
C. Hintermeier, C. Kirchner, and H. Kirchner.
Dynamically-Typed Computations for Order-Sorted Equational
Presentations.
In Proceedings of 7th International Workshop on Unification, UNIF'93,
Boston (MA, USA), 1993.
Also available as Technical Report 93-R-309, CRIN, Nancy (France).
C Kirchner, H. Kirchner, and M. Vittek.
Designing Constraint Logic Programming Languages using Computational
Systems.
In F. Orejas, editor, Proceedings of 2nd CCL Workshop, La Escala
(Spain), September 1993.
C. Kirchner, H. Kirchner, and M. Vittek.
Implementing Computational Systems with Constraints.
In P. Kanellakis, J.-L. Lassez, and V. Saraswat, editors, Proceedings of
1st Workshop on Principles and Practice of Constraint Programming, pages
166-175, Providence (RI, USA), 1993. Brown University.
Full paper
D. Lugiez and J.-L. Moysset.
Complement problems and tree automata in AC-like theories.
In P. Enjalbert, A. Finkel, and K.W. Wagner, editors, Proceedings of 10th
Annual Symposium on Theoretical Aspects of Computer Science, STACS'93,
volume 665 of Lecture Notes in Computer Science, pages 515-524,
Würzburg (Germany), February 1993. Springer-Verlag.
P. Narendran and M. Rusinowitch.
The Unifiability Problem in Ground AC Theories.
In Proceedings 8th IEEE Symposium on Logic in Computer Science, pages
364-370, Montréal (Québec, Canada), June 1993. IEEE Computer Society
Press.
Ch. Ringeissen.
Combinaison de Résolutions de Contraintes.
Thèse de Doctorat d'Université, Université Nancy 1, décembre 1993.
Full paper
L. Vigneron.
Basic AC-Paramodulation.
In F. Orejas, editor, Proceedings of 2nd CCL Workshop, La Escala
(Spain), September 1993.
Alexandre Boudet.
Combining Unification Algorithms.
Journal of Symbolic Computation, 16:597-626, 1993.
Val Breazu-Tannen, Delia Kesner, and Laurence Puel.
A typed pattern calculus.
Technical Report 878, Laboratoire de Recherche en Informatique, Univ.
Paris-Sud, France, 1993.
Full
paper
Hubert Comon.
Completion of Rewrite systems with membership constraints. Part I:
deduction rules.
This is a first part of a paper whose abstract appeared in Proc. ICALP 92,
Vienna. It will appear in the Journal of Symbolic Computation, August 1993.
Full
paper
Hubert Comon.
Completion of Rewrite systems with membership constraints. Part II:
Constraint Solving.
This is the second part of a paper whose abstract appeared in Proc. ICALP 92,
Vienna. It will appear in the Journal of Symbolic Computation, August 1993.
Full
paper
Hubert Comon.
Constraints in Term Algebras (Short Survey).
In T. Rus M. Nivat, C. Rattray and G. Scollo, editors, Proc. Conf. on
Algebraic Methodology and Software Technology, Workshop in Computing,
Univ. of Twente, 1993. Springer-Verlag.
Invited talk.
Full paper
Roberto Di Cosmo and Delia Kesner.
A confluent reduction for the extensional typed lambda-calculus with
pairs, sums, recursion and terminal object.
In Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors, 20th
International Colloquium on Automata, Languages and Programming, July
1993 (see there), pages 645-656.
Full paper
Maribel Fernández.
AC-Complement Problems: Satisfiability and Negation
Elimination.
In Claude Kirchner, editor, 5th International Conference on Rewriting
Techniques and Applications, June 1993 (see there), pages 358-373.
Maribel Fernández.
Modèles de calculs multiparadigmes fondés sur la réécriture.
Thèse de doctorat, Université Paris-Sud, Orsay, France, December 1993.
M. C. Gaudel and J.-P. Jouannaud, editors.
4th International Joint Conference on Theory and Practice of Software
Development, volume 668 of Lecture Notes in Computer Science,
Orsay, France, April 1993. Springer-Verlag.
Marianne Haberstrau.
ECOLOG: un Environnement pour la programmation en LOGique COntrainte.
Thèse de doctorat, Université Paris-Sud, Orsay, France, December 1993.
Delia Kesner.
La définition de fonctions par cas à l'aide de motifs dans des langages
applicatifs.
Thèse de doctorat, Université Paris-Sud, Orsay, France, December 1993.
Claude Kirchner, editor.
5th International Conference on Rewriting Techniques and Applications,
volume 690 of Lecture Notes in Computer Science, Montreal, Canada,
June 1993. Springer-Verlag.
Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors.
20th International Colloquium on Automata, Languages and Programming,
volume 700 of Lecture Notes in Computer Science, Lund, Sweden, July
1993. Springer-Verlag.
Claude Marché.
Réécriture modulo une théorie présentée par un système
convergent et décidabilité des problèmes du mot dans certaines classes
de théories équationnelles.
Thèse de doctorat, Université Paris-Sud, Orsay, France, October 1993.
Full paper Abstract
Walid Sadfi.
Contribution à l'étude de la séquentialité forte des définitions
de fonctions par règles.
Thèse de doctorat, Université Paris-Sud, Orsay, France, December 1993.
Stephen van Bakel and Maribel Fernández.
Strong Normalization of Typeable Rewrite Systems.
In Proceedings of HOA'93 (Higher Order Algebra), Lecture Notes In
Computer Science, vol. 816, Amsterdam, Holland, 1993. Springer-Verlag.
Peter Barth.
Linear 0-1 Inequalities and Extended Clauses.
In A. Voronkov, editor, Proceedings 4th International Conference on Logic
Programming and Automated Reasoning LPAR '93, volume 698 of Lecture
Notes in Computer Science, pages 40-51, St. Petersburg, Russia, 1993.
Springer.
Leo Bachmair and Harald Ganzinger.
Associative-Commutative Superposition.
Research Report MPI-I-93-267, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, December 1993.
Revised version in Proc. CTRS, LNCS 968.
Leo Bachmair and Harald Ganzinger.
Ordered Chaining for Total Orderings.
Research Report MPI-I-93-250, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, December 1993.
Short version in Proc. CADE'94, LNAI 814, pp. 435-450, 1994.
Leo Bachmair and Harald Ganzinger.
Rewrite Techniques for Transitive Relations.
Research Report MPI-I-93-249, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, November 1993.
Short version in Proc. LICS'94, pp. 384-393, 1994.
Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder.
Basic Paramodulation.
Research Report MPI-I-93-236, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, September 1993.
Revised version in Information and Computation 121(2), pp. 172-192, 1995.
Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, and
Fernando Orejas.
Completion Subsystem.
In Berthold Hoffmann and Bernd Krieg-Brückner, editors, Program
Development by Specification and Transformation, The PROSPECTRA Methodology,
Language Family, and System, volume 680 of Lecture Notes in Computer
Science, chapter 4.3: Part III: The System, Chapter, pages 460-494.
Springer-Verlag, Berlin, 1993.
Leo Bachmair, Harald Ganzinger, and Uwe Waldmann.
Set Constraints are the Monadic Class.
In Eighth Annual IEEE Symposium on Logic in Computer Science, pages
75-83, Montreal, Canada, 1993. IEEE Computer Society Press.
Leo Bachmair, Harald Ganzinger, and Uwe Waldmann.
Superposition with simplification as a decision procedure for the monadic
class with equality.
In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors,
Computational Logic and Proof Theory, Third Kurt Gödel Colloquium,
KGC'93, volume 713 of Lecture Notes in Computer Science, pages
83-96, Brno, Czech Republic, 1993. Springer.
Revised version of Technical Report MPI-I-93-204.
Alexander Bockmayr, Stefan Krischer, and Andreas Werner.
Narrowing Strategies for Arbitrary Canonical Rewrite Systems.
Research Report MPI-I-93-233, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, July 1993.
Alexander Bockmayr.
0-1 Constraints and 0-1 Optimization.
In F. Benhamou, A. Colmerauer, and G. Smolka, editors, 3rd Workshop on
Constraint Logic Programming (WCLP '93), Marseille, France, 1993. Faculty
of Luminy.
Alexander Bockmayr.
Conditional Narrowing Modulo a Set of Equations.
Applicable Algebra in Engineering, Communication and Computing,
4(3):147-168, September 1993.
Alexander Bockmayr.
Embedding OR Techniques in Constraint Logic Programming.
In A. Karmann, K. Mosler, M. Schader, and G. Uebe, editors, Operations
Research '92. 17th Symposium on Operations Research, pages 252-254,
Hamburg, Germany, 1993. Physica-Verlag.
Alexander Bockmayr.
Logic Programming with Pseudo-Boolean Constraints.
In F. Benhamou and A. Colmerauer, editors, Constraint Logic
Programming-Selected Research, pages 327-350. MIT Press, 1993.
Also available as Research Report MPI-I-91-227.
Alexander Bockmayr and F. J. Radermacher.
Künstliche Intelligenz und Operations Research.
In O. Herzog, Th. Christaller, and D. Schütt, editors, Grundlagen und
Anwendungen der Künstlichen Intelligenz. 17. Fachtagung für
Künstliche Intelligenz, Informatik Aktuell, pages 249-254, Berlin,
Germany, 1993. Springer.
Alexander Bockmayr and F. J. Radermacher.
Künstliche Intelligenz und Operations Research.
Research Report MPI-I-93-234, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, September 1993.
Harald Ganzinger, Leo Bachmair, and Uwe Waldmann.
Superposition with Simplification as a Decision Procedure for the Monadic
Class with Equality.
Research Report MPI-I-93-204, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, February 1993.
Peter Graf and Christoph Meyer.
Extended Path-Indexing.
Research Report MPI-I-93-253, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, April 1993.
Michael Hanus.
Analysis of Nonlinear Constraints in CLP(R).
In David Scott Warren, editor, Proceedings of the 10th International
Conference on Logic Programming (ICLP '93), pages 83-99, Budapest,
Hungary, 1993. MIT Press.
Extended version to appear in New Generation Computing.
Michael Hanus.
Towards the Global Optimization of Functional Logic Programs.
In Proc. Workshop on Global Compilation, International Logic Programming
Symposium, pages 83-97, Vancouver, Canada, 1993.
Michael Hanus and Berthold Josephs.
A Debugging Model for Functional Logic Programs.
In Maurice Bruynooghe and Jaan Penjam, editors, Proc. 5th Intern. Symposium
on Programming Language Implementation and Logic Programming (PLILP '93),
volume 714 of Lecture Notes in Computer Science,, pages 28-43,
Tallinn, Estonia, October 1993. Springer-Verlag.
Also available as Research Report MPI-I-93-222.
Jürgen Stuber.
Computing Stable Models by Program Transformation.
Research Report MPI-I-93-257, Max-Planck-Institut für Informatik, Im
Stadtwald, D-66123 Saarbrücken, Germany, December 1993.
A. Werner, Alexander Bockmayr, and S. Krischer.
A Concept for the Implementation of LSE Narrowing.
In C. Beierle, editor, 9. Workshop Logische Programmierung, Hagen,
1993. FU Hagen, Informatik Bericht 146 - 10/1993.
A. Werner, Alexander Bockmayr, and S. Krischer.
How to Realize LSE Narrowing.
In A. Mück, editor, Proceedings of the 2nd International Workshop on
Functional/Logic Programming, Rattenberg, October 1993. LMU
München, Technical Report 9311.
A. Werner, Alexander Bockmayr, and S. Krischer.
How to Realize LSE Narrowing.
Technical Report 6/93, Fakultät für Informatik, Universität
Karlsruhe, Karlsruhe, 1993.
Christoph Weidenbach.
Extending the Resolution Method with Sorts.
In R. Bajcsy, editor, Proceedings of the 13th International Joint
Conference on Artificial Intelligence (IJCAI '93), volume 1, pages
60-65, Chambery, France, 1993. Morgan Kaufmann.
Christoph Weidenbach.
A New Sorted Logic.
In Hans Jürgen Ohlbach, editor, GWAI-92: Advances in Artificial
Inteligence, Proceedings 16th German Workshop on Artificial Intelligence,
volume 671 of Lecture Notes in Artificial Intelligence, pages 43-54,
Bonn, 1993. Springer-Verlag.
Tobias Nipkow.
Orthogonal Higher-Order Rewrite Systems are Confluent.
In M. Bezem and J.F. Groote, editors, Proc. Int. Conf. Typed Lambda
Calculi and Applications, volume 664 of Lecture Notes in Computer
Science, pages 306-317. Springer-Verlag, 1993.
Full
paper
Tobias Nipkow and Christian Prehofer.
Type Checking Type Classes.
In Proc. 20th ACM Symp. Principles of Programming Languages, pages
409-418. ACM Press, 1993.
Revised version to appear in J. Functional Programming.
Full
paper
J.C.González-Moreno.
A Correctness Proof for Warren's HO into FO Translation.
Research Report DIA 93/4, Departamento de Informática y Automática,
Facultad de Matemáticas (UCM), Av. Complutense s/n, Ciudad Universitaria,
Madrid E-28040 (SPAIN), March 1993.
Full paper Abstract
Rita Loogen, Francisco López-Fraguas, and Mario Rodríguez-Artalejo.
A Demand Driven Strategy for Lazy Narrowing.
In PLILP' 93, volume 714 of LNCS, pages 184-200, Tallin,
Estonia, 1993. Springer.
Full paper Abstract
Narciso Martí-Oliet and José Meseguer.
Rewriting Logic as a Logical and Semantic Framework.
Technical Report SRI-CSL-93-05, Computer Science Laboratory, SRI International,
August 1993.
Submitted for publication.
Abstract
Pilar Nivela and Robert Nieuwenhuis.
Practical results on the saturation of full first-order clauses:
Experiments with the Saturate system. (System description).
In C. Kirchner, editor, 5th International Conference on Rewriting
Techniques and Applications, LNCS 690, Montreal, Canada, June 16-18,
1993. Springer-Verlag.
Full paper
Marisa Navarro, Fernando Orejas, and Ana Sánchez.
On the Correctness of Modular Systems.
In G. Scollo, editor, AMAST 93, Enschede, Netherlands, June 1993.
Albert Rubio and Robert Nieuwenhuis.
A precedence-based total AC-compatible ordering.
In C. Kirchner, editor, 5th International Conference on Rewriting
Techniques and Applications, LNCS 690, pages 374-388, Montreal, Canada,
June 16-18, 1993.
Full paper