{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T07:18:09Z","timestamp":1648970289842},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1996,9]]},"DOI":"10.1007\/bf02127744","type":"journal-article","created":{"date-parts":[[2005,9,15]],"date-time":"2005-09-15T11:34:26Z","timestamp":1126784066000},"page":"95-131","source":"Crossref","is-referenced-by-count":1,"title":["On Skolemization in constrained logics"],"prefix":"10.1007","volume":"18","author":[{"given":"Hans-J\u00fcrgen","family":"B\u00fcrckert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Hollunder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Laux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02127744_CR1","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/0304-3975(86)90047-2","volume":"45","author":"H. A\u00eft-Kaci","year":"1986","unstructured":"H. A\u00eft-Kaci, An algebraic semantics approach to the effective resolution of type equations,Theoretical Computer Science 45 (1986) 293\u2013351.","journal-title":"Theoretical Computer Science"},{"key":"BF02127744_CR2","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0743-1066(86)90013-0","volume":"3","author":"H. A\u00eft-Kaci","year":"1986","unstructured":"H. A\u00eft-Kaci and R. Nasr, LOGIN: A logic programming language with built-in inheritance,Journal of Logic Programming 3 (1986) 185\u2013215.","journal-title":"Journal of Logic Programming"},{"key":"BF02127744_CR3","doi-asserted-by":"crossref","unstructured":"F. Baader, H.-J. B\u00fcrckert, B. Hollunder, W. Nutt and J.H. Siekmann, Concept logics, in:Proceedings of the Symposium on Computational Logics, Br\u00fcssel, Belgium (1990).","DOI":"10.1007\/978-3-642-76274-1_10"},{"issue":"2\u20133","key":"BF02127744_CR4","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0004-3702(92)90055-3","volume":"55","author":"Ch. Beierle","year":"1992","unstructured":"Ch. Beierle, U. Hedtst\u00fcck, U. Pletat, P.H. Schmitt and J. Siekmann, An order-sorted logic for knowledge representation systems,Artificial Intelligence 55(2\u20133) (1992) 149\u2013192.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"BF02127744_CR5","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1207\/s15516709cog0902_1","volume":"9","author":"R.J. Brachman","year":"1985","unstructured":"R.J. Brachman and J.G. Schmolze, An overview of the KL-ONE knowledge representation system,Cognitive Science 9(2) (1985) 171\u2013216.","journal-title":"Cognitive Science"},{"key":"BF02127744_CR6","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert,A Resolution Principle for a Logic with Restricted Quantifiers, LNAI, Vol. 568 (Springer, 1991).","DOI":"10.1007\/3-540-55034-8"},{"issue":"2","key":"BF02127744_CR7","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0004-3702(94)90027-2","volume":"66","author":"H.-J. B\u00fcrckert","year":"1994","unstructured":"H.-J. B\u00fcrckert, A resolution principle for constrained logics,Artificial Intelligence 66(2) (1994) 235\u2013271.","journal-title":"Artificial Intelligence"},{"key":"BF02127744_CR8","unstructured":"H.-J. B\u00fcrckert, B. Hollunder and A. Laux, Concept logics with function symbols, in:Proceedings of the 11th European Conference on Artificial Intelligence, Amsterdam, The Netherlands, ed. A. Cohn (Wiley, 1994) pp. 406\u2013410."},{"key":"BF02127744_CR9","unstructured":"C.C. Chang and H.J. Keisler,Model Theory (North-Holland, 1990)."},{"key":"BF02127744_CR10","volume-title":"Symbolic Logic and Theorem Proving","author":"C.-L. Chang","year":"1973","unstructured":"C.-L. Chang and R.C.-T. Lee,Symbolic Logic and Theorem Proving (Academic Press, London, 1973)."},{"key":"BF02127744_CR11","first-page":"633","volume":"607","author":"A.G. Cohn","year":"1992","unstructured":"A.G. Cohn, A many sorted logic with possibly empty sorts, in:11th International Conference on Automated Deduction, CADE-11, LNAI, Vol. 607 (Springer, 1992) pp. 633\u2013647.","journal-title":"LNAI"},{"key":"BF02127744_CR12","unstructured":"A. Colmerauer, Equations and inequations on finite and infinite trees, in:Proceedings of the 2nd International Conference on Fifth Generation Computer Systems (Tokyo, Japan, 1984) pp. 85\u201399."},{"key":"BF02127744_CR13","unstructured":"F.M. Donini, M. Lenzerini, D. Nardi and A. Schaerf, A hybrid system integrating datalog and concept languages, in:Proceedings of the 2nd Italian Conference on Artificial Intelligence, LNAI, Vol. 549 (Springer-Verlag, 1991). An extended version appeared also in the Working Notes of the AAAI Fall SymposiumPrinciples of Hybrid Reasoning (1991)."},{"key":"BF02127744_CR14","doi-asserted-by":"crossref","unstructured":"M. Fitting,First-Order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science (Springer, 1990).","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"BF02127744_CR15","unstructured":"A.M. Frisch, A general framework for sorted deduction: Fundamental results on hybrid reasoning, in:Proceedings on the First International Conference on Principles of Knowledge Representation and Reasoning (1989) pp. 126\u2013136."},{"key":"BF02127744_CR16","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0004-3702(91)90009-9","volume":"49","author":"A.M. Frisch","year":"1991","unstructured":"A.M. Frisch, The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning,Artificial Intelligence 49 (1991) 161\u2013198.","journal-title":"Artificial Intelligence"},{"key":"BF02127744_CR17","doi-asserted-by":"crossref","unstructured":"A.M. Frisch and R.B. Scherl, A constraint logic approach to modal deduction, in:Logics in Al, European Workshop JELIA '90, ed. J. Eijck (Springer, 1990) pp. 234\u2013250.","DOI":"10.1007\/BFb0018445"},{"key":"BF02127744_CR18","volume-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the 2nd International Conference","author":"A.M. Frisch","year":"1991","unstructured":"A.M. Frisch and R.B. Scherl, A general framework for modal deduction, in:Principles of Knowledge Representation and Reasoning: Proceedings of the 2nd International Conference, eds. J.A. Allen, R. Fikes and E. Sandewall (Morgan-Kaufman, San Mateo, CA, 1991)."},{"key":"BF02127744_CR19","volume-title":"Logical Foundations of Artificial Intelligence","author":"M.R. Genesereth","year":"1987","unstructured":"M.R. Genesereth and N.J. Nilsson,Logical Foundations of Artificial Intelligence (Morgan-Kaufman, San Mateo, CA, 1987)."},{"key":"BF02127744_CR20","unstructured":"J. Herbrand, Recherches sur la th\u00e9orie de la d\u00e9monstration,Travaux de la Societ\u00e9 des Sciences et des Lettres de Varsovie 33(128) (1930)."},{"key":"BF02127744_CR21","series-title":"SEKI Working Paper","volume-title":"Ein Schema f\u00fcr constraint-basierte relationale Wissensbasen","author":"M. H\u00f6hfeld","year":"1988","unstructured":"M. H\u00f6hfeld, Ein Schema f\u00fcr constraint-basierte relationale Wissensbasen, SEKI Working Paper SWP-88-7, University of Kaiserslautern, Kaiserslautern, Germany (1988)."},{"key":"BF02127744_CR22","series-title":"LILOG Report","volume-title":"Definite relations over constraint languages","author":"M. H\u00f6hfeld","year":"1988","unstructured":"M. H\u00f6hfeld and G. Smolka, Definite relations over constraint languages, LILOG Report 53, IWBS, Heidelberg, Germany (1988)."},{"key":"BF02127744_CR23","unstructured":"J. Jaffar and J.-L. Lassez, Constrained logic programming, in:Proceedings of the ACM Symposium on Principles of Programming Languages (1987) pp. 111\u2013119."},{"key":"BF02127744_CR24","volume-title":"Constraints and Modalities in Terminological Knowledge Representation Systems","author":"A. Laux","year":"1995","unstructured":"A. Laux,Constraints and Modalities in Terminological Knowledge Representation Systems, PhD Thesis, University of Saarland, Saarbr\u00fccken (1995)."},{"key":"BF02127744_CR25","doi-asserted-by":"crossref","unstructured":"J.W. Lloyd,Foundations of Logic Programming (Springer-Verlag, 1984).","DOI":"10.1007\/978-3-642-96826-6"},{"key":"BF02127744_CR26","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF01396685","volume":"145","author":"A. Oberschelp","year":"1962","unstructured":"A. Oberschelp, Untersuchungen zur mehrsortigen Quantorenlogik,Mathematische Annalen 145 (1962) 297\u2013333.","journal-title":"Mathematische Annalen"},{"key":"BF02127744_CR27","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin, Building in equational theories,Machine Intelligence 7 (1972) 73\u201390.","journal-title":"Machine Intelligence"},{"key":"BF02127744_CR28","first-page":"135","volume":"4","author":"G.A. Robinson","year":"1969","unstructured":"G.A. Robinson and L. Wos, Paramodulation and theorem-proving in first order theories with equality, in:Machine Intelligence, Vol. 4 (Edinburgh University Press, 1969) pp. 135\u2013150.","journal-title":"Machine Intelligence"},{"issue":"1","key":"BF02127744_CR29","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson, A machine-oriented logic based on the resolution principle,JACM 12(1) (1965) 23\u201341.","journal-title":"JACM"},{"key":"BF02127744_CR30","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BF01448954","volume":"115","author":"A. Schmidt","year":"1938","unstructured":"A. Schmidt, \u00dcber deduktive Theorien mit mehreren Sorten von Grunddingen,Mathematische Annalen 115 (1938) 485\u2013506.","journal-title":"Mathematische Annalen"},{"key":"BF02127744_CR31","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BF02054948","volume":"123","author":"A. Schmidt","year":"1951","unstructured":"A. Schmidt, Die Zul\u00e4ssigkeit der Behandlung mehrsortiger Theorien mittels der \u00fcblichen einsortigen Pr\u00e4dikatenlogik,Mathematische Annalen 123 (1951) 187\u2013200.","journal-title":"Mathematische Annalen"},{"key":"BF02127744_CR32","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df,Computational Aspects of an Order-Sorted Logic with Term Declarations, LNAI, Vol. 395 (Springer, 1989).","DOI":"10.1007\/BFb0024065"},{"key":"BF02127744_CR33","series-title":"LILOG Report","volume-title":"A feature logic with subsorts","author":"G. Smolka","year":"1988","unstructured":"G. Smolka, A feature logic with subsorts, LILOG Report 33, IWBS, IBM Deutschland, Stuttgart, Germany (1988)."},{"issue":"4","key":"BF02127744_CR34","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"M.E. Stickel, Automated deduction by theory resolution,Journal of Automated Reasoning 1(4) (1985) 333\u2013355.","journal-title":"Journal of Automated Reasoning"},{"key":"BF02127744_CR35","series-title":"Research Notes in Artificial Intelligence","volume-title":"A Many-Sorted Calculus Based on Resolution and Paramodulation","author":"C. Walther","year":"1987","unstructured":"C. Walther,A Many-Sorted Calculus Based on Resolution and Paramodulation, Research Notes in Artificial Intelligence (Pitman, London, 1987)."},{"issue":"1","key":"BF02127744_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/42267.45071","volume":"35","author":"C. Walther","year":"1988","unstructured":"C. Walther, A many-sorted unification,JACM 35(1) (1988) 1\u201317.","journal-title":"JACM"},{"key":"BF02127744_CR37","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, A new sorted logic, in:Proceedings of the 16th German AI-Conference, GWAI-92, LNAI, Vol. 671, ed. H.J. Ohlbach (Springer, 1992) pp. 43\u201354.","DOI":"10.1007\/BFb0018991"},{"key":"BF02127744_CR38","unstructured":"C. Weidenbach, Extending the resolution method with sorts, in:Proceedings of the 13th International Joint Conference on Artificial Intelligence, Chambery, France (Morgan-Kaufmann, 1993) pp. 60\u201365."},{"key":"BF02127744_CR39","first-page":"688","volume-title":"Proceedings of the 9th European Conference on Artificial Intelligence","author":"C. Weidenbach","year":"1990","unstructured":"C. Weidenbach and H.-J. Ohlbach, A resolution calculus with dynamic sort structures and partial functions, in:Proceedings of the 9th European Conference on Artificial Intelligence (Pitman, London, 1990) pp. 688\u2013693."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127744.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02127744\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127744","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T14:02:30Z","timestamp":1586440950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02127744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["BF02127744"],"URL":"https:\/\/doi.org\/10.1007\/bf02127744","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}