{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T13:13:08Z","timestamp":1648818788713},"reference-count":19,"publisher":"Informa UK Limited","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Non-Classical Logics"],"published-print":{"date-parts":[[1993,1]]},"DOI":"10.1080\/11663081.1993.10510794","type":"journal-article","created":{"date-parts":[[2012,5,30]],"date-time":"2012-05-30T08:02:48Z","timestamp":1338364968000},"page":"7-38","source":"Crossref","is-referenced-by-count":2,"title":["Foundations of a theorem prover for functional and mathematical uses"],"prefix":"10.1080","volume":"3","author":[{"given":"Javier","family":"Leach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susana","family":"Nieva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"301","reference":[{"key":"CIT0001","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/0304-3975(79)90034-3","volume":"9","author":"Aubin R.","year":"1979","journal-title":"Theoretical Computer Science"},{"key":"CIT0002","doi-asserted-by":"crossref","unstructured":"Bibel, W. 1990. \u201cPerspectives of automated deduction. Invited talk at CADE'10, Lecture Notes in Computer Science, Vol. 449\u201d.","DOI":"10.1007\/3-540-52885-7_104"},{"key":"CIT0003","unstructured":"Boyer, R. S. and Moore, J. S. 1988. \u201cA Computational Logic Handbook. Academic Press\u201d."},{"key":"CIT0004","volume-title":"Mathematical Logic.","author":"Ebbinghaus H. D.","year":"1984"},{"key":"CIT0005","unstructured":"Gerhart, S. L. 1980. \u201cet al. An overview of affirm: a specification and verification system. Information Processing, 80, North Holland\u201d."},{"key":"CIT0006","volume-title":"Mechanizing Programming Logics in Higher Order Logic. Current Trends in Hardware Verification and Automated Theorem Proving. 387\u2013439.","author":"Gordon M. J.C.","year":"1989"},{"key":"CIT0007","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-50940-2_38","volume":"352","author":"Hanus M.","year":"1989","journal-title":"Vol 2. Lecture Notes in Computer Science"},{"key":"CIT0008","unstructured":"Lindsay, P. A., Moore, R. C. and Ritchie, B. 1987. \u201cReview of existing theorem provers. Thechnical Report Series UMCS\u201d."},{"key":"CIT0009","unstructured":"Lovelan, D. W. 1983. \u201cAutomated Theorem Proving: After 25 Years. Contemporary Mathematics, 29, American Mathemat. Soc.\u201d."},{"key":"CIT0010","unstructured":"Manna, Z. 1974. \u201cMathematical Theory of Computation. Mc Graw-Hill\u201d."},{"key":"CIT0011","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"Milner R.","year":"1978","journal-title":"J. of Computer and System Sciences"},{"issue":"1","key":"CIT0012","first-page":"2235","volume":"2","author":"Nieva S.","year":"1989","journal-title":"Computerized Logic Teaching Bulletin"},{"key":"CIT0013","unstructured":"Nieva, S. 1991. \u201cUna l\u00f3gica computacional con polimorfismo y recursi\u00f3n y un sistema de deducci\u00f3n autom\u00e1tica basado en ella. Ph. Thesis, Fac. Matem\u00e1ticas UCM\u201d."},{"key":"CIT0014","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and Computation.","author":"Paulson L. C.","year":"1987"},{"key":"CIT0015","unstructured":"Prazmowski, K. and Rudnicki, P. 1988. \u201cMIZAR-MSE primer and user guide. Tech. Report 88\u201311, The University of Alberta, Dept. of Computing Science, Edmonton\u201d."},{"key":"CIT0016","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1007\/BFb0012801","volume":"140","author":"Scott D. S.","year":"1982","journal-title":"Lecture Notes in Computer Science"},{"key":"CIT0017","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic.","author":"Smullyan R. M.","year":"1968"},{"key":"CIT0018","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory.","author":"Stoy J. E.","year":"1977"},{"key":"CIT0019","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/3-540-15648-8_30","volume":"193","author":"Trybulec A.","year":"1985","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Journal of Applied Non-Classical Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.tandfonline.com\/doi\/pdf\/10.1080\/10256018808623883","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,29]],"date-time":"2019-06-29T07:06:45Z","timestamp":1561792005000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.tandfonline.com\/doi\/abs\/10.1080\/11663081.1993.10510794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,1]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993,1]]}},"alternative-id":["10.1080\/11663081.1993.10510794"],"URL":"https:\/\/doi.org\/10.1080\/11663081.1993.10510794","relation":{},"ISSN":["1166-3081","1958-5780"],"issn-type":[{"value":"1166-3081","type":"print"},{"value":"1958-5780","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,1]]}}}