{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:59Z","timestamp":1725471179686},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371045"},{"type":"electronic","value":"9783540371069"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11812289_5","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T08:23:44Z","timestamp":1159518224000},"page":"44-53","source":"Crossref","is-referenced-by-count":1,"title":["A Dynamic Poincar\u00e9 Principle"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Kerber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Ayer, A.J.: Language, Truth and Logic. Victor Gollancz Ltd., 2nd edn., London, UK 1951 edn.(1936)"},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.2307\/421013","volume":"3","author":"H. Barendregt","year":"1997","unstructured":"Barendregt, H.: The impact of the lambda calculus in logic and computer science. Bull. Symbolic Logic\u00a03(2), 181\u2013215 (1997)","journal-title":"Bull. Symbolic Logic"},{"issue":"5","key":"5_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1006\/jsco.2001.0455","volume":"32","author":"H. Barendregt","year":"2001","unstructured":"Barendregt, H., Cohen, A.M.: Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants. Journal of Symbolic Computation\u00a032(5), 3\u201322 (2001)","journal-title":"Journal of Symbolic Computation"},{"key":"5_CR4","unstructured":"Boole, G.: An Investigation of The Laws of Thought, Cambridge, UK., Macmillan, Barclay, & Macmillan, New York (reprinted by Dover Publication 1854) (1958)"},{"key":"5_CR5","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)"},{"key":"5_CR6","unstructured":"Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle, reprint in: Begriffsschrift und andere Aufs\u00e4tze, J.A., (ed.), Hildesheim. Also in Logiktexte, Berka, K., Kreiser, L. (eds.), pp. 82\u2013112 (1879)"},{"key":"5_CR7","volume-title":"A Mathematician\u2019s Apology","author":"G. Hardy","year":"1940","unstructured":"Hardy, G.: A Mathematician\u2019s Apology. Cambridge University Press, London (1940)"},{"key":"5_CR8","first-page":"1879","volume-title":"From Frege to G\u00f6del \u2013 A Source Book in Mathematical Logic","year":"1967","unstructured":"van Heijenoort, J. (ed.): From Frege to G\u00f6del \u2013 A Source Book in Mathematical Logic, pp. 1879\u20131931. Havard University Press, Cambridge, Massachusett (1967)"},{"key":"5_CR9","unstructured":"Huet, G., et al.: The Coq Theorem Prover (Version 8.0). \n                    \n                      http:\/\/coq.inria.fr\/doc-eng.html"},{"key":"5_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/11551263_30","volume-title":"KI 2005: Advances in Artificial Intelligence","author":"M. Kerber","year":"2005","unstructured":"Kerber, M.: Why is the Lucas-Penrose argument invalid? In: Furbach, U. (ed.) KI 2005. LNCS (LNAI), vol.\u00a03698, pp. 380\u2013393. Springer, Heidelberg (2005)"},{"issue":"3","key":"5_CR11","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1023\/A:1006059810729","volume":"21","author":"M. Kerber","year":"1998","unstructured":"Kerber, M., Kohlhase, M., Sorge, V.: Integrating computer algebra into proof planning. Journal of Automated Reasoning\u00a021(3), 327\u2013355 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR12","unstructured":"Leibniz, G.W.: Projet et essais pour arriver \u00e0 quelque certitude pour finir une bonne partie des disputes et pour avancer l\u2019art d\u2019inventer. In: Berka, K., Kreiser, L. (eds.). Logiktexte, ch. I.2, pp. 16\u201318. Akademie-Verlag, german translation, Berlin, Germany (1686) (1983)"},{"key":"5_CR13","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Selected Papers on Automath","year":"1994","unstructured":"Nederpelt, R., Geuvers, H., de Vrijer, R. (eds.): Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol.\u00a0133. North-Holland, Amsterdam (1994)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11812289_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:04Z","timestamp":1619508424000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11812289_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371045","9783540371069"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11812289_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}