{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:39:22Z","timestamp":1725799162135},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662441442"},{"type":"electronic","value":"9783662441459"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44145-9_10","type":"book-chapter","created":{"date-parts":[[2014,8,22]],"date-time":"2014-08-22T21:10:45Z","timestamp":1408741845000},"page":"137-151","source":"Crossref","is-referenced-by-count":4,"title":["Ancestral Logic: A Proof Theoretical Study"],"prefix":"10.1007","author":[{"given":"Liron","family":"Cohen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnon","family":"Avron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Aho, A.V., Ullman, J.D.: Universality of data retrieval languages. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 110\u2013119. ACM (1979)","DOI":"10.1145\/567752.567763"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Avron, A.: Transitive closure and the mechanization of mathematics. In: Kamareddine, F.D. (ed.) Thirty Five Years of Automating Mathematics. Applied Logic Series, vol.\u00a028, pp. 149\u2013171. Springer Netherlands (2003)","DOI":"10.1007\/978-94-017-0253-9_7"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-27818-4_3","volume-title":"Mathematical Knowledge Management","author":"A. Avron","year":"2004","unstructured":"Avron, A.: Formalizing set theory as it is actually used. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 32\u201343. Springer, Heidelberg (2004)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-78127-1_6","volume-title":"Pillars of Computer Science","author":"A. Avron","year":"2008","unstructured":"Avron, A.: A framework for formalizing set theories based on the use of static set terms. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol.\u00a04800, pp. 87\u2013106. Springer, Heidelberg (2008)"},{"key":"10_CR5","unstructured":"Campbell, J.J.J.A., Reis, J.C.G.D., Wenzel, P.S.M., Sorge, V.: Intelligent computer mathematics (2008)"},{"key":"10_CR6","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., Upper Saddle River (1986)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite Model Theory, vol.\u00a02. Springer (1995)","DOI":"10.1007\/3-540-28788-4"},{"key":"10_CR8","unstructured":"Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets (1974)"},{"key":"10_CR9","unstructured":"Gentzen, G.: Neue Fassung des Widerspruchsfreiheitsbeweises f\u00fcr die reine Zahlentheorie. Forschungen zur Logik\u00a04, 19\u201344 (1969); English translation in: Szabo, M.E.: The collected work of Gerhard Gentzen. North-Holland, Amsterdam"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Kamareddine, F.D.: Thirty five years of automating mathematics, vol.\u00a028. Springer (2003)","DOI":"10.1007\/978-94-017-0253-9"},{"issue":"1","key":"10_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2267976","volume":"8","author":"R.M. Martin","year":"1943","unstructured":"Martin, R.M.: A homogeneous system for formal logic. The Journal of Symbolic Logic\u00a08(1), 1\u201323 (1943)","journal-title":"The Journal of Symbolic Logic"},{"issue":"1","key":"10_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.2307\/2268974","volume":"14","author":"R.M. Martin","year":"1949","unstructured":"Martin, R.M.: A note on nominalism and recursive functions. The Journal of Symbolic Logic\u00a014(1), 27\u201331 (1949)","journal-title":"The Journal of Symbolic Logic"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-24849-1_19","volume-title":"Types for Proofs and Programs","author":"A. Momigliano","year":"2004","unstructured":"Momigliano, A., Tiu, A.: Induction and co-induction in sequent calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 293\u2013308. Springer, Heidelberg (2004)"},{"issue":"3","key":"10_CR14","doi-asserted-by":"publisher","first-page":"192","DOI":"10.2307\/2267692","volume":"17","author":"J. Myhill","year":"1952","unstructured":"Myhill, J.: A derivation of number theory from ancestral theory. The Journal of Symbolic Logic\u00a017(3), 192\u2013197 (1952)","journal-title":"The Journal of Symbolic Logic"},{"key":"10_CR15","unstructured":"Rudnicki, P.: An overview of the mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311\u2013330 (1992)"},{"key":"10_CR16","unstructured":"Shapiro, S.: Foundations without Foundationalism: A Case for Second-Order Logic: A Case for Second-Order Logic. Oxford University Press (1991)"},{"issue":"297","key":"10_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/analys\/68.1.1","volume":"68","author":"P. Smith","year":"2008","unstructured":"Smith, P.: Ancestral arithmetic and isaacson\u2019s thesis. Analysis\u00a068(297), 1\u201310 (2008)","journal-title":"Analysis"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Tiu, A., Momigliano, A.: Cut elimination for a logic with induction and co-induction. Journal of Applied Logic\u00a010(4), 330\u2013367 (2012); Selected papers from the 6th International Conference on Soft Computing Models in Industrial and Environmental Applications","DOI":"10.1016\/j.jal.2012.07.007"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44145-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T13:07:08Z","timestamp":1558962428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44145-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662441442","9783662441459"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44145-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}