{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:50Z","timestamp":1725664490685},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540620341"},{"type":"electronic","value":"9783540496311"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-62034-6_56","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:31:40Z","timestamp":1330277500000},"page":"274-285","source":"Crossref","is-referenced-by-count":1,"title":["Higher-order proof by consistency"],"prefix":"10.1007","author":[{"given":"Henrik","family":"Linnestad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Prehofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olav","family":"Lysne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Canonical Equational Proofs. Birkh\u00c4user, 1991.","DOI":"10.1007\/978-1-4684-7118-2"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"E. Bevers and J. Lewi. Proof by consistency in conditional equational theories. In Proc. 2nd International Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lect. Not. in Comp. Sci., pages 194\u2013205. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-54317-1_91"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK), July 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"L. Fribourg. A strong restriction on the inductive completion procedure. In Proc. 13th International Colloquium on Automata, Languages and Programming, volume 226 of Lect. Not. in Comp. Sci., pages 105\u2013115. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16761-7_60"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"J. A. Goguen. How to prove inductive hypotheses without induction. In W. Bibel and R. Kowalski, editors, Proc. of the 5th Conference on Automated Deduction, volume 87 of Lect. Not. in Comp. Sci., pages 356\u2013373. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle et al., editor, VLSI Specification, Verification and Synthesis. Kluwer Academic Press, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"issue":"2","key":"24_CR8","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2):239\u2013266, 1982.","journal-title":"Journal of Computer and System Sciences"},{"key":"24_CR9","unstructured":"J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in equational theories without constructors. In Proc. Logic in Computer Science, pages 358\u2013366, 1986."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and A. Rubio. A recursive path ordering for higher-order terms in \u03b7-long \u0392-normal form. In H. Ganzinger, editor, Proc. 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lect. Not. in Comp. Sci. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61464-8_46"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"S. Kahrs. Towards a domain theory for termination proofs. In Proc. of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lect. Not. in Comp. Sci., pages 241\u2013255. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59200-8_60"},{"issue":"4","key":"24_CR12","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"D. Kapur, P. Narendran, and H. Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395\u2013415, 1987.","journal-title":"Acta Informatica"},{"key":"24_CR13","volume-title":"Mathematical Centre Tracts 127","author":"J. W. Klop","year":"1980","unstructured":"J. W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts 127, Mathematisch Centrum,Amsterdam, 1980."},{"key":"24_CR14","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, 1970."},{"key":"24_CR15","unstructured":"C. A. Lor\u00eda-S\u00e1enz. A Theoretical Framework for Reasoning about Program Construction Based on Extensions of Rewrite Systems. PhD thesis, Universit\u00c4t Kaiserslautern, 1993."},{"key":"24_CR16","first-page":"276","volume-title":"volume 632 of Lect. Not. in Comp. Sci.","author":"O. Lysne","year":"1992","unstructured":"O. Lysne. Proof by consistency in constructive systems with final algebra semantics. In Proc. 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy), volume 632 of Lect. Not. in Comp. Sci., pages 276\u2013290. Springer-Verlag, 1992."},{"key":"24_CR17","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0020-0190(94)00109-X","volume":"51","author":"O. Lysne","year":"1994","unstructured":"O. Lysne. Extending Bachmair's method for proof by consistency to the final algebra. Information Processing Letters, 51:303\u2013310, 1994.","journal-title":"Information Processing Letters"},{"key":"24_CR18","first-page":"26","volume-title":"volume 914 of Lect. Not. in Comp. Sci.","author":"O. Lysne","year":"1995","unstructured":"O. Lysne and J. Piris. A termination ordering for higher order rewrite systems. In Proc. 6th Conference on Rewriting Techniques and Applications, Kaiserslautern (Germany), volume 914 of Lect. Not. in Comp. Sci., pages 26\u201340. Springer-Verlag, 1995."},{"key":"24_CR19","unstructured":"R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Technical report, Institut f\u00fcr Informatik, Technische Universit\u00c4t M\u00fcnchen, August 1994. To appear in Theoretical Computer Science."},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Extensions of Logic Programming, volume 475 of Lect. Not. in Comp. Sci., pages 253\u2013281. Springer-Verlag, 1991.","DOI":"10.1007\/BFb0038698"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"D. L. Musser. On proving inductive properties in abstract data types. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, pages 154\u2013162, January 1980.","DOI":"10.1145\/567446.567461"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proc. of the 6th IEEE Symposium on Logic in Computer Science, pages 342\u2013359, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Not. in Comp. Sci. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"24_CR24","first-page":"635","volume-title":"volume 814 of Lect. Not. in Art. Intell.","author":"C. Prehofer","year":"1994","unstructured":"C. Prehofer. Decidable higher-order unification problems. In Proc. 12th International Conference on Automated Deduction, Nancy, volume 814 of Lect. Not. in Art. Intell., pages 635\u2013649. Springer-Verlag, 1994."},{"key":"24_CR25","unstructured":"C. Prehofer. Solving Higher-Order Equations: From Logic to Programming. PhD thesis, Technische Universit\u00c4t M\u00fcnchen, 1995."},{"key":"24_CR26","first-page":"162","volume-title":"volume 449 of Lect. Not. in Comp. Sci.","author":"U. S. Reddy","year":"1990","unstructured":"U. S. Reddy. Term rewriting induction. In Proc. 10th International Conference on Automated Deduction, Kaiserslautern, volume 449 of Lect. Not. in Comp. Sci., pages 162\u2013177. Springer-Verlag, 1990."},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"J. van de Pol. Termination proofs for higher-order rewrite systems. In 1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting, volume 816 of Lecture Notes in Computer Science, pages 305\u2013325. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-58233-9_14"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62034-6_56.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:11:38Z","timestamp":1605629498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62034-6_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540620341","9783540496311"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-62034-6_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}