Unification in many-sorted equational theories

1. Buettner, W., "Unification in the datastructure multiset", Journal of Automated Reasoning, vol.2, pp. 75–88, (1986).

   Article  Google Scholar 

2. Buettner,W., "Unification in the datastructure set", (to appear in this Proc. of 8^th CADE)

   Google Scholar 

3. Cunningham, R.J., Dick, A.J.J., "Rewrite Systems on a Lattice of Types", Rep. No. DOC 83/7, Imperial College, London SW7 (1983)

   Google Scholar 

4. Cohn, A.G. "Improving the Expressiveness of Many-sorted Logic.", AAAI-83, Washington (1983)

   Google Scholar 

5. Fages, F. "Formes canonique dans les algèbres booleènnes et application à la dèmonstration automatique en logique de premier ordre." Thèse du 3^eme cycle, Paris, (1983)

   Google Scholar 

6. Goguen, J.A., Meseguer, J., "Equality, Types, Modules and Generics for Logic Programming", Journal of Logic Programming, (1984)

   Google Scholar 

7. Goguen, J.A., Meseguer, J., "Order Sorted Algebra I. Partial and Overloaded Operators, Errors and Inheritance.", SRI Report (1985)

   Google Scholar 

8. Grätzer, G., "Universal algebra", Springer Verlag, (1979)

   Google Scholar 

9. Hayes, P., "A Logic of Actions.", Machine Intelligence 6, Metamathematics Unit, University of Edinburgh (1971)

   Google Scholar 

10. Herold, A., "Some basic notions of first order unification theory.", Internal report 15/83, Univ. Karlsruhe, (1983)

    Google Scholar 

11. Herold, A.,Siekmann, J., "Unification in abelian semigroups", technical report, Universität Kaiserslautern, Memo SEKI-85-III, (1985)

    Google Scholar 

12. Henschen, L.J., "N-Sorted Logic for Automated Theorem Proving in Higher-Order Logic.", Proc. ACM Conference Boston, (1972)

    Google Scholar 

13. Huet, G., "Resolution d'equations dans des languages d'ordere 1,2,..., ω;";, These d'Etat, Univ. de Paris, VII, (1976)

    Google Scholar 

14. Huet, G., Oppen, D.C., "Equations and Rewrite Rules", SRI Technical Report CSL-111, (1980)

    Google Scholar 

15. Hullot, J.M., "Canonical forms and unification," Proc of the 5 ^th workshop on automated deduction, Springer Lecture Notes, vol. 87, pp. 318–334, (1980)

    Google Scholar 

16. Karl Mark G. Raph, "The Markgraf Karl Refutation Procedure", Technical report, Univ. Kaiserslautern, Memo SEKI-84-03, (1984)

    Google Scholar 

17. Loveland, D., "Automated Theorem Proving", North Holland, (1980)

    Google Scholar 

18. Livesey,M., Siekmann, J., "Unification of sets and multisets," Technical report, Unive Kaiserslautern, Memo-SEKI-76-01, (1976)

    Google Scholar 

19. Oberschelp, A., "Untersuchungen zur mehrsortigen Quantorenlogik.", Mathematische Annalen 145 (1962)

    Google Scholar 

20. Plotkin, G., "Building in equational theories.", Machine Intelligence, vol. 7, 1972

    Google Scholar 

21. Robinson, J.A., "A Machine-Oriented Logic Based on the Resolution Principle." JACM 12 (1965)

    Google Scholar 

22. Schmidt-Schauss, M., "A many-sorted calculus with polymorphic functions based on resolution and paramodulation.", Proc 9 ^th IJCAI, Los Angeles,(1985)

    Google Scholar 

23. Schmidt-Schauss, M., "Unification in a many-sorted calculus with declarations.", Proc. of GWAI, (1985)

    Google Scholar 

24. Schmidt-Schauss, M., "Unification in many-sorted equational theories.", Internal report. Institut für Informatik, Kaiserslautern (forthcoming)

    Google Scholar 

25. Siekmann, J. H., "Universal Unification", Proc. of the 7 ^th CADE, Napa California, (1984)

    Google Scholar 

26. Stickel, M.E., "A unification algorithm for Associative-Commutative Functions", JACM 28, pp. 423–434, (1981)

    Article  Google Scholar 

27. Szabo, P., "Theory of First order Unification.", (in German, thesis) Univ. Karlsruhe, 1982

    Google Scholar 

28. Walther, C., "A Many-Sorted Calculus Based on Resolution and Paramodulation.", Proc. of the 8 ^th I JCAI, Karlsruhe, (1983)

    Google Scholar 

29. Walther, C., "Unification in Many-Sorted Theories.", Proc. of the 6 ^th ECAI, PISA, (1984)

    Google Scholar 

Download references