{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T22:37:27Z","timestamp":1648679847818},"reference-count":17,"publisher":"Informa UK Limited","issue":"1-2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Non-Classical Logics"],"published-print":{"date-parts":[[1998,1]]},"DOI":"10.1080\/11663081.1998.10510935","type":"journal-article","created":{"date-parts":[[2012,5,30]],"date-time":"2012-05-30T08:12:32Z","timestamp":1338365552000},"page":"123-140","source":"Crossref","is-referenced-by-count":1,"title":["A Shell for Generic Interactive Proof Search"],"prefix":"10.1080","volume":"8","author":[{"given":"Aleksey","family":"Novodvorsky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksey","family":"Smirnov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"301","reference":[{"key":"CIT0001","unstructured":"Rasiowa, H. and Sikorski, R. 1963. \u201cThe Mathematics of Metamathematics, Warszawa\u201d."},{"key":"CIT0002","unstructured":"Barwise, J. and Etchemendy, J. 1994. \u201cHyperproof. CSLI\u201d."},{"key":"CIT0003","unstructured":"MacLogic. 1991. \u201cMALT project St Andrews University\u201d."},{"key":"CIT0004","volume-title":"The number systems","author":"Feferman S.","year":"1963"},{"key":"CIT0005","unstructured":"Smirnov, V. 1972. \u201cFormal inference and logical calculus, Moscow\u201d. (in Russian)"},{"key":"CIT0006","unstructured":"Smirnov, V. 1990. \u201cMoscow\u201d. Logic and computer. (in Russian)"},{"key":"CIT0007","unstructured":"Smirnov, A. and Novodvorsky, A. 1993. \u201cLogical systems description language, ILCSDP, Moscow\u201d."},{"key":"CIT0008","doi-asserted-by":"crossref","unstructured":"Suppes, P. 1990. \u201cUses of Artificial Intelligence in computer-based instruction. In Artificial Intelligence in Higher Education. Springer-Verlag\u201d.","DOI":"10.1007\/3-540-52952-7_27"},{"key":"CIT0009","unstructured":"Constable, R. L. 1986. \u201cImplementing Mathematics with the NuPRL proof development system\u201d. Prentice-Hall\u201d. \u2022."},{"key":"CIT0010","unstructured":"Dowek, G. 1991. \u201cThe Coq Proof Assistant User's Guide\u201d. Rapport Technique INRIA\u201d. \u2022."},{"key":"CIT0011","unstructured":"Caferra, R. and Herment, M. 1993. \u201cGLEFatinf, A Graphic Framework for Combining Provers and Editing Proofs for Different Logics,\u201d Proc. DISG'0'93, LNCS 722, Springer-Verlag\u201d. \u2022"},{"key":"CIT0012","doi-asserted-by":"crossref","unstructured":"Trybulec, A. and Blair, H. 1985. \u201cComputer aided reasoning\u201d. Logic of programs, Brooklyn\u201d. \u2022 LNCS 193","DOI":"10.1007\/3-540-15648-8_30"},{"key":"CIT0013","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Kahn, G. and Thery, L. 1994. \u201cProof by Pointing\u201d Proc. TACS'94, LNCS 789, Springer-Verlag\u201d. \u2022","DOI":"10.1007\/3-540-57887-0_94"},{"key":"CIT0014","volume-title":"\u201cDesign and implementation of symbolic computation systems, Proc. IFIP W.G. 2.5 Conference","author":"Limongelli C.","year":"1991"},{"key":"CIT0015","doi-asserted-by":"crossref","DOI":"10.1007\/BF00248324","volume":"5","author":"Paulson L. C.","year":"1989","journal-title":"Journal of automated reasoning"},{"key":"CIT0016","volume-title":"Proc. of the 2nd Annual Logic in Computer Sc. Conf","author":"Harper R.","year":"1987"},{"key":"CIT0017","volume-title":"Proc 7th Int. Conf on Logic Programming","author":"Sawamura H.","year":"1990"}],"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:08:09Z","timestamp":1561792089000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.tandfonline.com\/doi\/abs\/10.1080\/11663081.1998.10510935"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,1]]},"references-count":17,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1998,1]]}},"alternative-id":["10.1080\/11663081.1998.10510935"],"URL":"https:\/\/doi.org\/10.1080\/11663081.1998.10510935","relation":{},"ISSN":["1166-3081","1958-5780"],"issn-type":[{"value":"1166-3081","type":"print"},{"value":"1958-5780","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,1]]}}}