Abstract
This paper provides an introduction to many-sorted logics and motivates their use for representation and reasoning. Perhaps the most important reason to be interested in many-sorted logic is that computational efficiency can be achieved because the search space can be smaller and the length of a derivation shorter than in unsorted logic. There are many possible many-sorted logics of varying degrees of expressiveness, and the dimensions in which many-sorted logics differ are outlined and logics at various points in this space described. The relationship of many-sorted logic to unsorted logic is discussed and the reason why many-sorted logics derivations may be shorter is demonstrated. The paper concludes with a discussion of some many-sorted logic programming languages and some implementation issues.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Aït-Kaci, H. & Nasr, R. (1985) LOGIN: A Logic Programming Language with Built-in Inheritance. AI-068-85, Microelectronics and Computer Technology Corporation.
Aït-Kaci, H. & Lincoln, P. (1988) LIFE: a Natural Languege for Natural Language, Report ACA-ST-074–88, Microelectronics and Computer Technology Corporation, Austin, Texas.
Allen, J.F. & Miller, B.W. (1986) The HORNE Reasoning System in COMMON LISP. TR126 (Revised), University of Rochester.
Antoniou, G. & Ohlbach, H. (1983) Terminator, In Proceedings of the IJCAI 1983, Morgan Kaufmann, Calif.
Bibel, W., Letz, R. & Schumann, J. (1987) Bottom-up Enhancements of Deductive Systems. Conference on Artificial Intelligence and Information-Control Systems of Robots, Amsterdam, North Holland.
Bobrow, D. & Winograd, T. (1977) Experience with KRL-0: one cycle of a knowledge representation language. In Proceedings of the IJCAI 1977, pp. 213–222. Morgan Kaufmann, Los Altos Calif.
Brachman, R.J. (1985) “I Lied about the Trees” or, Defaults and Definitions in Knowledge Representation. The AI Magazine, 6, 80–93.
Bratko, I. (1986) Prolog Programming for Artificial Intelligence. Addison Wesley, Wokingham.
Bundy, A., Byrd, L., Luger, G., Mellish, C. & Palmer, M. (1979) Solving Mechanics Problems Using Metalevel Inference. In Proceedings of the IJCAI 6, Tokyo.
Bundy, A., Byrd, L. & Mellish, C. (1982) Special Purpose, but Domain Independent, Inference Mechanisms. In Proceedings of the ECAI, University of Edinburgh.
Bundy, A. (1983a) Turning the Search Space Inside Out, AI Department Internal Research Note 196, University of Edinburgh.
Bundy, A. (1983b) The Computer Modelling of Mathematical Reasoning. Academic Press, London.
Burstall, R.M. & Gougen, J.A. (1977) Putting Theories Together to Make Specifications. In Proceedings of the IJCAI 1977, pp. 1045–1058. Morgan Kaufmann, Los Altos Calif.
Chaminade, G. (1988) Some Computational Aspects of an Order Sorted Calculus: Order Sorted Unification Using Compact Representation of Clauses. In Proceedings of the ECAI, pp. 625–630, Pitman, London.
Champeaux, D. de, (1978) A Theorem Prover Dating a Semantic Network. In Proceedings of the AISB/GI Conference on AI, Hamburg.
Cohn, A.G. (1983a) Improving the Expressiveness of Many Sorted Logic. In Proceedings of the AAAI, Washington DC.
Cohn, A.G. (1983b) Mechanising a Particularly Expressive Many Sorted Logic. PhD Thesis, University of Essex.
Cohn, A.G. (1985) On the Solution of Schubert's Steamroller in Many Sorted Logic. In Proceedings of the IJCAI 9, Los Angeles.
Cohn, A.G. (1986) Many Sorted Logic = Unsorted Logic + Control? In Research and Development in Expert Systems 86, (ed M. Bramer), pp. 184–194. Cambridge University Press, 1986.
Cohn, A.G. (1987) A More Expressive Formulation of Many Sorted Logic. J. Automated Reasoning, Vol. 3, 2, 113–200.
Cunningham, J. (1985) A Methodology and a Tool for the Formalization of ‘Common Sense’ (Naive Physical) Knowledge. PhD Thesis, University of Essex.
Cunningham, R.J. & Dick, A.J.J. (1985) Rewrite systems on a Lattice of Types. Acta Informatica, 22, 149–169.
Dahl, V. (1977) Un System Deductif d'Interrogation de Banques de Donnes en Espagnol. Technical Report, Groupe d'Intelligence Artificielle, Univ of Marseille-Luminy.
Davies, N. (1987) Schubert's Steamroller in a Natural Deduction System. In Research and Development in Expert Systems IV, (ed S. Moralee), Cambridge University Press.
Dayantis, G. (1988) Types, Modularisation and Abstraction in Logic Programming. DPhil Thesis, University of Sussex.
Doyle, J. (1979) A truth Truth maintenance system. Artificial Intelligence, 12, 231–272.
Enderton, H.B. (1972) A Mathematical Introduction to Logic. Academic Press, New York.
Findler, N. (1979) Associative Networks. Academic Press, New York.
Frisch, A.M. (1985) An Investigation into Inference with Restricted Quantification and a Taxonomic Representation. SIGART Newsletter, 91, 28–31.
Frisch, A.M. (1986) Parsing with Restricted Quantification: An Initial Demonstration. In Artificial Intelligence and its Applications. (Eds A.G.Cohn & J.R.Thomas), pp. 5–22. John Wiley, Chichester.
Frisch, A.M. (1987) Knowledge Retrieval as Specialised Inference. TR 214, University of Rochester.
Futatsugi, K., Goguen, J.A., Jouannaud, J.A. & Meseguer, J. (1985) Principles of OBJ2. In Proceedings of Principles in Programming Languages, pp. 52–66, ACM.
Genesereth, M. & Nilsson, N. (1987) Logical Foundations of Artificial Intelligence. Morgan Kaufmann, Los Altos Calif.
Goguen, J.A. (1978) Order Sorted Algebra. Semantics and Theory of Computation Report 14, UCLA.
Goguen, J.A. & Meseguer, J. (1984) Equalities, Types, Modules and Generics for Logic Programming, Journal of Logic Programming, 1, 179–210.
Goguen, J.A. & Meseguer, J. (1985) Order Sorted Algebra 1: Partial and Overloaded Operators, SRI International, Palo Alto, Calif.
Goossens, D. (1986) Automatic Node Recognition in a Particition Graph: restricting the search space while preserving completeness. In Proceedings of the ECAI, Brighton.
Gordon, M., Milner, R., Morris, L., Newey, M. & Wadsworth, C. (1978) A Metalanguage for Interactive Proof in LCF. In Proceedings of the Fifth ACM SIGACT-SIGPLAN Conference on Principles of Programming Languages, Tueson, Arizona.
Green, C.C. (1969) The application of theorem proving techniques to question answering systems. In Proceedings of the IJCAI, pp. 219–237, Morgan Kaufmann, Los Altos.
Hailperin, T. (1957a) A Theory of Restricted Quantification. J. Symbolic Logic, 22, 19–35.
Hailperin, T. (1957b) A Theory of Restricted Quantification II. J. Symbolic Logic, 22, 113–129.
Hayes, P.J. (1971) A Logic of Actions. In Machine Intelligence 6, Edinburgh University Press.
Hayes, P.J. (1979) The Logic of Frames. In Frame Conceptions and Text Understanding. (Ed D.Metzing), pp. 46–61, Walter de Gruyter and Company, Berlin.
Hayes, P.J. (1985) Ontology of liquids. In Formal Theories of the Commonsense World (eds J.Hobbs & R.Moore), pp. 71–107. Ablex, Norwood, New Jersey.
Herbrand, J. (1971) Logical Writings, Havard University Press.
Hudson, R.A. (1971) English Complex Sentences: an Introduction to Systemic Grammar. North Holland.
Levesque, H.J. (1986) Making Believers out of Computers. Artificial Intelligence, 30, 81–108.
Levesque, H.J. & Brachman, R.J. (1987) Expressiveness and Tractability in Knowledge Representation and Reasoning. Computational Intelligence, 3, 78–93.
McCarthy, J. (1968) Programs with Common Sense. In Semantic Information Processing. (Ed M.Minsky), MIT Press, Cambridge, Mass.
McDermott, D. (1982) A Temporal Logic for Reasoning about Processes and Plans. Cognitive Science, 6, 101–156.
McDermott, D. (1987) A Critique of Pure Reason. Computational Intelligence, 3, 151–160.
McSkimin, J.R. & Minker, J. (1977) The Use of a Semantic Network in a Deductive Question Answering System. In Proceedings of the IJCAI 5, Cambridge, Mass, Morgan Kaufmann, Los Altos, Calif.
Mellish, C. (1988) Implementing Systemic Classification by Unification. Computational Linguistics, 14, (1) 40–51.
Michalski, R.S. (1988) A Theory and Methodology of Inductive Learning. In Machine Learning: An Artificial Intelligence Approach. (Ed R.Michalski, C.Carbonell & T.Mitchell), pp. 83–134, Tioga Publishing Company, Palo Alto.
Minsky, M. (1975) A framework for representing knowledge. In The Psychology of Computer Vision. (Ed P.Winston), McGraw Hill, New York.
Mycroft, A. & O'Keefe, R.A. (1984) A Polymorphic Type System for Prolog. Artificial Intelligence, 23, 295–308.
O'Keefe, R.A. (1984) A New Data Structure for Type Trees. In Proceedings of the ECAI, Elsevier, Amsterdam.
Oberschelp, A. (1962) Untersuchungen zur Mehrsortigen Quantorenlogik. Math. Annalen, 145, 297–333.
Ohlbach, H.J. & Schmidt-Schauss, M. (1985) The lion and the unicorn. J. Automated Reasoning, 1, 327–332.
Plotkin, G. (1970) A Note on Inductive Generalisation. In Machine Intelligence 5.
Reiter, R. (1981) On the Integrity of Typed First Order Data Bases. In Advances in Data Base Theory, Volume 1. (Eds H.Gallaire, J.Minker & J.M.Nicolas), Plenum Press, London.
Robinson, J.A. & Wos, L.T. (1969) Paramodulation and Theorem Proving in First Order Theories with Equality. In Machine Intelligence 4, pp. 135–150. Edinburgh University Press.
Schmidt-Schauss, M. (1985) A Many Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. In Proceedings of the IJCAI, Los Angeles, Morgan Kaufmann, Los Altos, Calif.
Schmidt-Schauss, M. (1986) Unification in Many Sorted Equational Theories. In Eighth International Conference on Automated Deduction, pp. 538–552, Springer Verlag, Berlin.
Schmidt-Schauss, M. (1988) Computational Aspects of an Order Sorted Logic with Term Declarations. SEKI report SR-88–10, Universitaet Kaiserslautern, FGR.
Schmidt, A. (1938) Uber Deduktive Theorien mit Mehren Sorten von Grunddingen. Math. Annalen, 115, 485–506.
Schmidt, A. (1951) Die Zuelassigkeit der Behandlung Mehrsortiger Theorien Mittels der Ublichen Einsortigen Pradikatenlogik. Math. Annalen, 123, 187–200.
Siekmann, J. (1986) Unification Theory. In Proceedings of the ECAI, Brighton, 1986.
Smolka, G. (1986) Order-Sorted Horn Logic: Semantics and Deduction. SEKI-REPORT SR-86-17, Universitaet Kaiserslautern.
Smolka, G. (1987) TEL (Version 0.9) Report and User Manual. SEKI-Report SR-87–11, Universitaet Kaiserslautern, FGR.
Smolka, G., Nutt, W., Goguen, J.A. & Meseguer, J. (1987) Order-Sorted Equational Computation. SEKI-Report SR-87–14, Universitaet Kaiserslautern, FGR.
Smolka, G. & Aït-Kaci, H. (1987) Inheritance Hierarchies: Semantics and Unification. Technical Report AI-057-87, MicroElectronics and Computer Technology Corporation.
Smullyan, R. (1978) What is the Name of this Book? Pelican, Harmondsworth.
Steels, L. (1985) Introduction To the Knowledge Representation System KRS, Vrije Universiteit, Brussels.
Stickel, M.E. (1986) Schubert's Steamroller Problem: Formulations and Solutions. J. Automated Reasoning, 2, 85–101.
Strachey, C. (1967) Fundamental Concepts in Programming Languages. Unpublished Notes for a Nato Summer School, Copenhagen, Denmark.
Veronis, J. (1987) Discourse Consistency and Many Sorted Logic. In Proceedings of the IJCAI, Milan, Morgan Kaufmann, Los Altos, Calif.
Walther, C. (1983) A Many Sorted Calculus Based on Resolution and Paramodulation. In Proceedings of the IJCAI 8, Karlsruhe.
Walther, C. (1985) A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution. Artificial Intelligence, 26, 217–224.
Walther, C. (1986) A Classification of Unification Problems in Many Sorted Theories. In Proceedings of the CADE; Lecture notes in computer science 230, Springer Verlag, Heidelberg.
Walther, C. (1987) A Many Sorted Calculus Based on Resolution and Paramodulation. Pitman.
Wang, H. (1952) Logic of Many Sorted Theories. J. Symbolic Logic, 17, (2), 105–116.
Winograd, T. (1975) Frame Representations and the Declarative/Procedural Controversy. In Representation and Understanding: Studies in Cognitive Science. (Eds D.G.Bobrow & A.Collins), pp. 185–210. Academic Press, New York.
Wos, L., Overbeek, R., Lusk, E. & Boyle, J. (1984) Automated Reasoning: Introduction and Applications. Prentice Hall, Englewood Cliffs, New Jersey.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Cohn, A.G. Taxonomic reasoning with many-sorted logics. Artif Intell Rev 3, 89–128 (1989). https://doi.org/10.1007/BF00128778
Issue Date:
DOI: https://doi.org/10.1007/BF00128778