{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T14:21:47Z","timestamp":1649082107850},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1985,3,1]],"date-time":"1985-03-01T00:00:00Z","timestamp":478483200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["BIT"],"published-print":{"date-parts":[[1985,3]]},"DOI":"10.1007\/bf01934987","type":"journal-article","created":{"date-parts":[[2005,7,25]],"date-time":"2005-07-25T05:43:43Z","timestamp":1122270223000},"page":"51-64","source":"Crossref","is-referenced-by-count":1,"title":["Automated theorem proving methods"],"prefix":"10.1007","volume":"25","author":[{"given":"Rolf","family":"Nossum","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"BF01934987_CR1","doi-asserted-by":"crossref","unstructured":"M. Davis,The prehistory and early history of automated deduction, in vol. 1 of Siekmann & Wrightson (eds): \u201cAutomation of Reasoning\u201d 1\u20132, Springer 1983.","DOI":"10.1007\/978-3-642-81952-0_1"},{"key":"BF01934987_CR2","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/BF01458217","volume":"76","author":"L. L\u00f6wenheim","year":"1915","unstructured":"L. L\u00f6wenheim, \u00dcber M\u00f6glichkeiten im Relativkalk\u00fcl, Mathematische Annalen 76, 1915, pp. 447\u2013470.","journal-title":"Mathematische Annalen"},{"key":"BF01934987_CR3","unstructured":"T. Skolem,Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit und Beweisbarkeit mathematischen S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen, Kristiania Vitenskapsselskaps Skrifter, nr. 4, 1920, pp. 1\u201336."},{"key":"BF01934987_CR4","unstructured":"T. Skolem,\u00dcber die mathematische Logik, Norsk matematisk tidsskrift, nr. 10, 1928, pp. 125\u2013142."},{"key":"BF01934987_CR5","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"P. C. Gilmore","year":"1960","unstructured":"P. C. Gilmore,A proof method for quantification theory: its justification and realisation, IBM Journal of Research and Development 4, 1960, pp. 28\u201335.","journal-title":"IBM Journal of Research and Development"},{"key":"BF01934987_CR6","unstructured":"J. Herbrand,Recherches sur la th\u00e9orie de la d\u00e9monstration, Th\u00e8ses pr\u00e9sent\u00e9es \u00e0 la facult\u00e9 des sciences de Paris, 1930."},{"key":"BF01934987_CR7","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"D. Prawitz,An improved proof procedure, Theoria 26, 1960, pp. 102\u2013139.","journal-title":"Theoria"},{"key":"BF01934987_CR8","unstructured":"B. Dreben and W. D. Goldfarb,The Decision Problem, Addison-Wesley, 1979."},{"key":"BF01934987_CR9","first-page":"230","volume":"42","author":"A. Turing","year":"1936","unstructured":"A. Turing,On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society 42, 1936, pp. 230\u2013265.","journal-title":"Proceedings of the London Mathematical Society"},{"key":"BF01934987_CR10","doi-asserted-by":"crossref","first-page":"40","DOI":"10.2307\/2269326","volume":"1","author":"A. Church","year":"1936","unstructured":"A. Church,A note on the Entscheidungsproblem, Journal of Symbolic Logic 1, 1936, pp. 40\u201341.","journal-title":"Journal of Symbolic Logic"},{"key":"BF01934987_CR11","unstructured":"R. Nossum,Decision algorithms for program verification, University of Oslo, 1984."},{"key":"BF01934987_CR12","doi-asserted-by":"crossref","unstructured":"E. Eder,Properties of substitutions and unifications, Technische Universit\u00e4t M\u00fcnchen, 1983.","DOI":"10.1007\/978-3-642-69391-5_18"},{"key":"BF01934987_CR13","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, Journal of the ACM 12, 1965, pp. 23\u201341.","journal-title":"Journal of the ACM"},{"key":"BF01934987_CR14","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. S. Paterson","year":"1978","unstructured":"M. S. Paterson and M. N. Wegman,Linear unification, Journal of Computer and System Sciences, 16, 1978, pp. 158\u2013167.","journal-title":"Journal of Computer and System Sciences"},{"key":"BF01934987_CR15","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"R. Kowalski,A proof procedure using connection graphs, Journal of the ACM 22, 1975, pp. 572\u2013595.","journal-title":"Journal of the ACM"},{"key":"BF01934987_CR16","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BFb0060634","volume":"125","author":"D. Prawitz","year":"1968","unstructured":"D. Prawitz,A proof procedure with matrix reduction, Lecture Notes in Mathematics 125, 1968, pp. 207\u2013213.","journal-title":"Lecture Notes in Mathematics"},{"key":"BF01934987_CR17","first-page":"933","volume":"8","author":"J. A. Kalman","year":"1983","unstructured":"J. A. Kalman and J. G. Peterson,Computer-aided studies of all possible single axioms for the equivalential calculus, Proceedings of the IJCAI 8, 1983, pp. 933\u2013935.","journal-title":"Proceedings of the IJCAI"},{"key":"BF01934987_CR18","first-page":"569","volume":"74","author":"R. Kowalski","year":"1974","unstructured":"R. Kowalski,Predicate logic as a programming language, Information Processing 74, 1974, pp. 569\u2013574.","journal-title":"Information Processing"},{"key":"BF01934987_CR19","unstructured":"R. Overbeek, L. Wos, E. Lusk and J. Boyle,Automated Reasoning, Prentice-Hall, 1984."},{"key":"BF01934987_CR20","unstructured":"K. M. G. Raph,The Markgraf Karl refutation procedure, University of Kaiserslautern, 1984."},{"key":"BF01934987_CR21","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel,On matrices with connections, Journal of the ACM 28, 1981, pp. 633\u2013645.","journal-title":"Journal of the ACM"},{"key":"BF01934987_CR22","doi-asserted-by":"crossref","unstructured":"M. Davis and H. Putnam,A computing procedure for quantification theory, Journal of the ACM 7, 1960, pp. 201 ff.","DOI":"10.1145\/321033.321034"},{"key":"BF01934987_CR23","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"P. B. Andrews,Theorem proving via general matings, Journal of the ACM 28, 1981, pp. 193\u2013214.","journal-title":"Journal of the ACM"},{"key":"BF01934987_CR24","doi-asserted-by":"crossref","unstructured":"W. Bibel,Automated Theorem Proving, Vieweg Verlag, 1982.","DOI":"10.1007\/978-3-322-90100-2"},{"key":"BF01934987_CR25","unstructured":"E. Eder,An implementation of a theorem prover based on the connection method, Technische Universit\u00e4t M\u00fcnchen, 1984."}],"container-title":["BIT"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01934987.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01934987\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01934987","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T10:01:15Z","timestamp":1586340075000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01934987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985,3]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1985,3]]}},"alternative-id":["BF01934987"],"URL":"https:\/\/doi.org\/10.1007\/bf01934987","relation":{},"ISSN":["0006-3835","1572-9125"],"issn-type":[{"value":"0006-3835","type":"print"},{"value":"1572-9125","type":"electronic"}],"subject":[],"published":{"date-parts":[[1985,3]]}}}