{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:18:44Z","timestamp":1725455924652},"publisher-location":"Berlin\/Heidelberg","reference-count":14,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055873X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013832","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:24:11Z","timestamp":1132730651000},"page":"276-290","source":"Crossref","is-referenced-by-count":1,"title":["Proof by consistency in constructive systems with final algebra semantics"],"prefix":"10.1007","author":[{"given":"Olav","family":"Lysne","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","volume-title":"Technical Report 106","author":"O.-J. Dahl","year":"1986","unstructured":"O.-J. Dahl, Dag F. Langmyhr, and O. Owe. Preliminary report on the specification and programming language ABEL. Technical Report 106, Informatics Department, University of Oslo, Norway, 1986."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"J.A. Goguen. How to prove inductive hypotheses without induction. In W. Bibel and R. Kowalski, editors, Proceedings of the Fifth Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 356\u2013373. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"18_CR3","unstructured":"J.V. Guttag. The Specification and Application to Programming of Abstract Data Types. PhD thesis, Computer Science Department, University of Toronto, 1975."},{"key":"18_CR4","unstructured":"J.V. Guttag, J.J. Horning, and J.M. Wing. Larch in five easy pieces. Technical report, Digital Systems Research Center, 1985."},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, pages 239\u2013266, 1982.","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"18_CR6","unstructured":"J.-P. Jouannaud and E. Kounalis. Automatic proofs in theories without constructors. Technical Report 295, Universite de Paris-Sud, Centre d'Orsay, septembre 1986."},{"issue":"1","key":"18_CR7","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/357195.357202","volume":"5","author":"S. Kamin","year":"1983","unstructured":"S. Kamin. Final data types and their specification. ACM Transactions on Programming Languages and Systems, 5(1):97\u2013123, January 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"18_CR8","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"D. Kapur and R. Musser. Proof by consistency. Artificial Intelligence, 31:125\u2013157, 1987.","journal-title":"Artificial Intelligence"},{"issue":"4","key":"18_CR9","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1093\/comjnl\/26.4.289","volume":"26","author":"P. Lescanne","year":"1983","unstructured":"P. Lescanne. Behavioural categoricity of abstract data type specifications. The Computer Journal, 26(4):289\u2013292, 1983.","journal-title":"The Computer Journal"},{"key":"18_CR10","series-title":"Technical report 163","volume-title":"PhD thesis","author":"O. Lysne","year":"1991","unstructured":"O. Lysne. Term Rewriting Techniques for Systems based on Generator Induction. PhD thesis, Informatics Department, University of Oslo, Norway, 1991. Technical report 163."},{"key":"18_CR11","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":"18_CR12","volume-title":"PhD thesis","author":"O. Owe","year":"1980","unstructured":"O. Owe. A specification Technique with Idealization. PhD thesis, Informatics Department, University of Oslo, Norway, March 1980."},{"key":"18_CR13","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"D. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182\u2013215, 1985.","journal-title":"Information and Control"},{"key":"18_CR14","unstructured":"L. Puel. Proof in the final algebra. In B. Courcelle, editor, Proceedings 9th Colloquium on Trees in Algebra and Programming, pages 227\u2013242. Cambridge University Press, 1984."}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0013832.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:08:11Z","timestamp":1607353691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055873X"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0013832","relation":{},"subject":[]}}