{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,30]],"date-time":"2024-05-30T13:46:22Z","timestamp":1717076782163},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bf00881919","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:40:00Z","timestamp":1104003600000},"page":"267-275","source":"Crossref","is-referenced-by-count":9,"title":["A note on assumptions about Skolem functions"],"prefix":"10.1007","volume":"15","author":[{"given":"Hans J\ufffdrgen","family":"Ohlbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic","author":"B. F. Chellas","year":"1980","unstructured":"Chellas, B. F.:Modal Logic, Cambridge Univ. Press, Cambridge, 1980."},{"key":"CR2","volume-title":"Automated Theorem Proving: A Logical Basis, Vol. 6 ofFundamental Studies in Computer Science","author":"D. Loveland","year":"1978","unstructured":"Loveland, D.:Automated Theorem Proving: A Logical Basis, Vol. 6 ofFundamental Studies in Computer Science, North-Holland, Amsterdam, 1978."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"McCune, W.: Otter 2.0, in10th Int. Conf. on Automated Deduction, CADE-10, Vol. 449 ofLNCS, Springer, 1990, pp. 663?664.","DOI":"10.1007\/3-540-52885-7_131"},{"key":"CR4","unstructured":"Nonnengart, A.: First-order modal logic theorem proving and functional simulation, inProc. of 13th Int. Joint Conf. on Artificial Intelligence, IJCAI-93, Morgan Kaufmann, 1993, pp. 80?85."},{"issue":"5","key":"CR5","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"Hans J\u00fcrgen Ohlbach","year":"1991","unstructured":"Ohlbach, Hans J\u00fcrgen: Semantics-based translation methods for modal logics,J. Logic and Computation 1(5) (1991), 691?746.","journal-title":"J. Logic and Computation"},{"issue":"2","key":"CR6","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J.: Seventy-five problems for testing automatic theorem provers,J. Automated Reasoning 2(2) (1986), 191?216, Errata:J. Automated Reasoning 4(2) (1988), 235?236.","journal-title":"J. Automated Reasoning"},{"key":"CR7","unstructured":"Scherl, R. B.: A constrained logic approach to automated modal deduction, Internal Report UIUCDCS-R-93-1803, University of Illinois at Urbana-Champaign, May 1993."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Schmidt-Schau\u00df, M.:Computational Aspects of an Order Sorted Logic with Term Declarations, Vol. 395 ofLNAI, Springer, 1989.","DOI":"10.1007\/BFb0024065"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Walther, C.:A Many-sorted Calculus based on Resolution and Paramodulation, Research Notes in Artificial Intelligence, Pitman Ltd., 1987.","DOI":"10.1016\/B978-0-273-08718-2.50007-9"},{"key":"CR10","series-title":"MPI-Report","volume-title":"A sorted logic using dynamic sorts","author":"C. Weidenbach","year":"1991","unstructured":"Weidenbach, C.: A sorted logic using dynamic sorts, MPI-Report MPI-I-91-218, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, December 1991."},{"key":"CR11","unstructured":"Weidenbach, C.: Extending the resolution method with sorts, inProc. of 13th Int. Joint Conf. on Artificial Intelligence, IJCAI-93, Morgan Kaufmann, 1993, pp. 60?65."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881919.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881919\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:30:07Z","timestamp":1586043007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":11,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF00881919"],"URL":"https:\/\/doi.org\/10.1007\/bf00881919","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}