{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:17Z","timestamp":1725663677959},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569923"},{"type":"electronic","value":"9783540478904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56992-8_12","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T06:59:34Z","timestamp":1330239574000},"page":"167-181","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning with higher order partial functions"],"prefix":"10.1007","author":[{"given":"A.","family":"Gavilanes-Franco","sequence":"first","affiliation":[]},{"given":"F.","family":"Lucio-Carrasco","sequence":"additional","affiliation":[]},{"given":"M.","family":"Rodr\u00edguez-Artalejo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"12_CR1","first-page":"445","volume":"4","author":"A. Arnold","year":"1980","unstructured":"A. Arnold, M. Nivat. The metric space of infinite trees. Algebraic and topological properties. Ann. Soc. Math. Polon. Ser. IV Fund. Inform. 4, 445\u2013476, 1980.","journal-title":"Ann. Soc. Math. Polon. Ser. IV Fund. Inform."},{"key":"12_CR2","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF00264250","volume":"22","author":"H. Barringer","year":"1984","unstructured":"H. Barringer, J. H. Cheng, C. B. Jones. A logic covering undefinedness in program proofs. Acta Informatica 22, 251\u2013269, 1984.","journal-title":"Acta Informatica"},{"key":"12_CR3","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BF00625280","volume":"18","author":"M. Broy","year":"1982","unstructured":"M. Broy, M. Wirsing. Partial Abstract Types. Acta Informatica 18, 47\u201364, 1982.","journal-title":"Acta Informatica"},{"key":"12_CR4","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. J. Symbolic Logic 5, 56\u201368, 1940.","journal-title":"J. Symbolic Logic"},{"key":"12_CR5","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF01982047","volume":"12","author":"H.-D- Ebbinghaus","year":"1969","unstructured":"H.-D-Ebbinghaus. \u00dcber eine Pr\u00e4dikatenlogik mit partiell definierten Pr\u00e4dikaten und Funktionen. Arch. Math. Logik 12, 39\u201353, 1969.","journal-title":"Arch. Math. Logik"},{"key":"12_CR6","unstructured":"H.-D. Ebbinghaus, J. Flum, W. Thomas. Mathematical Logic. Springer-Verlag, 1984."},{"issue":"3","key":"12_CR7","doi-asserted-by":"crossref","first-page":"1269","DOI":"10.2307\/2274487","volume":"55","author":"W. M. Farmer","year":"1990","unstructured":"W. M. Farmer. A partial function version of Church's simple theory of types. J. Symbolic Logic 55 (3), 1269\u20131291, 1990.","journal-title":"J. Symbolic Logic"},{"issue":"4","key":"12_CR8","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0743-1066(85)80005-4","volume":"2","author":"M. Fitting","year":"1985","unstructured":"M. Fitting. A Kripke-Kleene semantics for logic programs. J. Logic Programming 2 (4), 295\u2013312, 1985.","journal-title":"J. Logic Programming"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"12_CR10","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0304-3975(90)90005-3","volume":"74","author":"A. Gavilanes-Franco","year":"1990","unstructured":"A. Gavilanes-Franco, F. Lucio-Carrasco. A first order logic for partial functions. Theoretical Computer Science 74, 37\u201369, 1990.","journal-title":"Theoretical Computer Science"},{"key":"12_CR11","first-page":"73","volume-title":"VLSI specification, verification, and synthesis","author":"M. J. Gordon","year":"1987","unstructured":"M. J. Gordon. HOL: a proof generating system for higher-order logic. In VLSI specification, verification, and synthesis. (G. Birtwistle, P. A. Subrahmanyam, eds.). Kluwer, Dordrecht, 73\u2013128, 1987."},{"key":"12_CR12","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"L. Henkin. Completeness in the theory of types. J. Symbolic Logic 15, 81\u201391, 1950.","journal-title":"J. Symbolic Logic"},{"key":"12_CR13","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/0304-3975(91)90334-X","volume":"79","author":"M. Holden","year":"1991","unstructured":"M. Holden. Weak logic theory. Theoretical Computer Science 79, 295\u2013321, 1991.","journal-title":"Theoretical Computer Science"},{"key":"12_CR14","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/BF00292109","volume":"24","author":"A. Hoogewijs","year":"1987","unstructured":"A. Hoogewijs. Partial-predicate logic in computer science. Acta Informatica 24, 281\u2013293, 1987.","journal-title":"Acta Informatica"},{"key":"12_CR15","unstructured":"J. R. Hindley, J. P. Seldin. Introduction to Combinators and \u03bb-calculus. Cambridge University Press, 1986."},{"key":"12_CR16","unstructured":"S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952."},{"key":"12_CR17","unstructured":"B. Krieg-Br\u00fcckner et al. PROSPECTRA Project Summary. University of Bremen, 1985."},{"key":"12_CR18","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0743-1066(87)90007-0","volume":"4","author":"K. Kunen","year":"1987","unstructured":"K. Kunen. Negation in logic programming. J. Logic Programming 4, 289\u2013308, 1987.","journal-title":"J. Logic Programming"},{"key":"12_CR19","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/3-540-50214-9_19","volume":"328","author":"B. Konikowska","year":"1988","unstructured":"B. Konikowska, A. Tarlecki and A. Blikle. A three-valued logic for software specification and validation.In Proc. VDM'88, VDM-The Way Ahead. LNCS 328, 218\u2013242, 1988.","journal-title":"Proc. VDM'88, VDM-The Way Ahead. LNCS"},{"issue":"4","key":"12_CR20","doi-asserted-by":"crossref","first-page":"646","DOI":"10.1145\/29873.30399","volume":"9","author":"J. Loeckx","year":"1987","unstructured":"J. Loeckx. Algorithmic specifications: A constructive specification method for abstract data types. ACM Trans. Prog. Lang. 9 (4), 646\u2013685, 1987.","journal-title":"ACM Trans. Prog. Lang."},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"J. McCarthy. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems. North-Holland, 33\u201370, 1963.","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"12_CR22","unstructured":"G. Nadathur, D. Miller. An overview of \u03bb-prolog. Procs. ICLP'88. The MIT Press, 810\u2013827, 1988."},{"key":"12_CR23","unstructured":"B. Nordstr\u00f6m, K. Peterson, J. M. Smith. Programming in Martin-L\u00f6f's Type Theory. Oxford Science Publications, 1990."},{"key":"12_CR24","unstructured":"O. Owe. An approach to program reasoning based on a first-order logic for partial functions. Comp. Sc. Techn. Report No CS-081. Dep. Elect. Engien. and Comp. Sc., Univ. of California, 1984."},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Logic and computation. Interactive proof with Cambridge LCF. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"12_CR26","unstructured":"The PRL group (Constable et al.). Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986."},{"key":"12_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. M. Smullyan","year":"1968","unstructured":"R. M. Smullyan. First-Order Logic. Springer, Berlin, 1968."},{"key":"12_CR28","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF01887213","volume":"1","author":"S. Thompson","year":"1989","unstructured":"S. Thompson. A Logic for Miranda. Formal Aspects of Computing 1, 339\u2013365, 1989.","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56992-8_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:58:00Z","timestamp":1619557080000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56992-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569923","9783540478904"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-56992-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}