Skip to main content
Log in

Taxonomic reasoning with many-sorted logics

  • Published:
Artificial Intelligence Review Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • Brachman, R.J. (1985) “I Lied about the Trees” or, Defaults and Definitions in Knowledge Representation. The AI Magazine, 6, 80–93.

    Google Scholar 

  • Bratko, I. (1986) Prolog Programming for Artificial Intelligence. Addison Wesley, Wokingham.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • Enderton, H.B. (1972) A Mathematical Introduction to Logic. Academic Press, New York.

    Google Scholar 

  • Findler, N. (1979) Associative Networks. Academic Press, New York.

    Google Scholar 

  • Frisch, A.M. (1985) An Investigation into Inference with Restricted Quantification and a Taxonomic Representation. SIGART Newsletter, 91, 28–31.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • Goguen, J.A. & Meseguer, J. (1985) Order Sorted Algebra 1: Partial and Overloaded Operators, SRI International, Palo Alto, Calif.

    Google Scholar 

  • 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.

    Google Scholar 

  • Hailperin, T. (1957a) A Theory of Restricted Quantification. J. Symbolic Logic, 22, 19–35.

    Google Scholar 

  • Hailperin, T. (1957b) A Theory of Restricted Quantification II. J. Symbolic Logic, 22, 113–129.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • Levesque, H.J. & Brachman, R.J. (1987) Expressiveness and Tractability in Knowledge Representation and Reasoning. Computational Intelligence, 3, 78–93.

    Google Scholar 

  • McCarthy, J. (1968) Programs with Common Sense. In Semantic Information Processing. (Ed M.Minsky), MIT Press, Cambridge, Mass.

    Google Scholar 

  • McDermott, D. (1982) A Temporal Logic for Reasoning about Processes and Plans. Cognitive Science, 6, 101–156.

    Google Scholar 

  • McDermott, D. (1987) A Critique of Pure Reason. Computational Intelligence, 3, 151–160.

    Google Scholar 

  • 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.

    Google Scholar 

  • Mellish, C. (1988) Implementing Systemic Classification by Unification. Computational Linguistics, 14, (1) 40–51.

    Google Scholar 

  • 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.

    Google Scholar 

  • Minsky, M. (1975) A framework for representing knowledge. In The Psychology of Computer Vision. (Ed P.Winston), McGraw Hill, New York.

    Google Scholar 

  • Mycroft, A. & O'Keefe, R.A. (1984) A Polymorphic Type System for Prolog. Artificial Intelligence, 23, 295–308.

    Google Scholar 

  • O'Keefe, R.A. (1984) A New Data Structure for Type Trees. In Proceedings of the ECAI, Elsevier, Amsterdam.

    Google Scholar 

  • Oberschelp, A. (1962) Untersuchungen zur Mehrsortigen Quantorenlogik. Math. Annalen, 145, 297–333.

    Google Scholar 

  • Ohlbach, H.J. & Schmidt-Schauss, M. (1985) The lion and the unicorn. J. Automated Reasoning, 1, 327–332.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • Schmidt-Schauss, M. (1986) Unification in Many Sorted Equational Theories. In Eighth International Conference on Automated Deduction, pp. 538–552, Springer Verlag, Berlin.

    Google Scholar 

  • Schmidt-Schauss, M. (1988) Computational Aspects of an Order Sorted Logic with Term Declarations. SEKI report SR-88–10, Universitaet Kaiserslautern, FGR.

    Google Scholar 

  • Schmidt, A. (1938) Uber Deduktive Theorien mit Mehren Sorten von Grunddingen. Math. Annalen, 115, 485–506.

    Google Scholar 

  • Schmidt, A. (1951) Die Zuelassigkeit der Behandlung Mehrsortiger Theorien Mittels der Ublichen Einsortigen Pradikatenlogik. Math. Annalen, 123, 187–200.

    Google Scholar 

  • 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.

    Google Scholar 

  • Smolka, G., Nutt, W., Goguen, J.A. & Meseguer, J. (1987) Order-Sorted Equational Computation. SEKI-Report SR-87–14, Universitaet Kaiserslautern, FGR.

    Google Scholar 

  • 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.

    Google Scholar 

  • Steels, L. (1985) Introduction To the Knowledge Representation System KRS, Vrije Universiteit, Brussels.

    Google Scholar 

  • Stickel, M.E. (1986) Schubert's Steamroller Problem: Formulations and Solutions. J. Automated Reasoning, 2, 85–101.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • Wos, L., Overbeek, R., Lusk, E. & Boyle, J. (1984) Automated Reasoning: Introduction and Applications. Prentice Hall, Englewood Cliffs, New Jersey.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints 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

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00128778

Keywords

Navigation