{"entities":{"Q1179807":{"pageid":1190556,"ns":120,"title":"Item:Q1179807","lastrevid":69815727,"modified":"2026-04-13T09:34:44Z","type":"item","id":"Q1179807","labels":{"en":{"language":"en","value":"Context induction: A proof principle for behavioural abstractions and algebraic implementations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 26474"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$29EB8FBD-BADB-48B7-A2EB-EB265D2DDD85","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7618fe49c48582241c0b586a5492e40758f6abff","datavalue":{"value":{"text":"Context induction: A proof principle for behavioural abstractions and algebraic implementations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1179807$73CE5EF1-6938-40CF-ABAC-C7665F849818","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"022acffcc5c401d05c380e1bd0161e22c5155c1f","datavalue":{"value":"0739.68060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1179807$6FE34AC9-029A-42A0-A490-EDD79D23DA03","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b01ac610e568696643824911668dec3af2c7b3d1","datavalue":{"value":"10.1007/BF01642507","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1179807$16650F12-C944-4D22-8968-686861B9AA10","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"82d7e2ad3382677d83b89ec58edf18af8299f3c0","datavalue":{"value":{"entity-type":"item","numeric-id":549176,"id":"Q549176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$ED09B380-E720-419C-8263-4D96627B39B4","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$9875BF6C-5218-4111-8561-F7CFB02F410C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70844ffc4666eabac4e20376c648613dbe8620f7","datavalue":{"value":{"time":"+1992-06-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1179807$2BA262B7-81F8-42A0-AB37-D5838FDAADA1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cbbb4185131237ae459c29c7d9fb47bb18adb722","datavalue":{"value":"A context induction method is proposed and discussed. The method is appropriate for proving behavioural properties of data types. The motivation is supported by the fact that from a program user's point of view, internal data representations are not relevant if they induce the same observable effects. The applications for the proof technique using context induction principle are discussed as well. It is proposed to use context induction as a uniform proof principle in the process of formal program development.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1179807$C1A931E4-1B1C-4CEB-A740-B7456D58C94C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1179807$E8D299ED-B991-4A3E-95E9-71311440C3EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1179807$4E056E91-A2D1-4B44-A4DC-39A0B69B8A60","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5c914cc35ba8bcd9c2781cc04c0a13717459d2b6","datavalue":{"value":"26474","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1179807$F747B996-E8EE-494E-BEBB-367D310E1394","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca1a231e3b3cc441d78d2f6754d104dbd78e7a6d","datavalue":{"value":"behavioural specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1179807$6D3F8503-9C9F-4FBD-BCA6-7D07C63030A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c62003a03bbad2b053e809cedb628edbfb092e1b","datavalue":{"value":"behavioural theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1179807$E114D46E-45F5-4CFF-A9A1-DC5143E051CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0e5e7f8dea8964138436b8564651a5cc1b89825","datavalue":{"value":"behavioural implementation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1179807$6ABFE1F9-0981-45F1-A720-112124A81E31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f134e05380bdf241e222701ec0f0a525c3166ab","datavalue":{"value":"FRI implementation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1179807$CA7E38DF-ADC5-49F0-8DEE-6D0F588C7A62","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$AD006F8E-F438-468B-AF05-81E61969F42E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$130C4325-1890-467F-B63F-D3FEE17AC166","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"839654c16ca8a6f2e87e45cf7258a92c536a3e2c","datavalue":{"value":{"entity-type":"item","numeric-id":1079358,"id":"Q1079358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$2BB6E156-BBB0-4013-A8B1-659524F1BA76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3209dcffb68253e20194ca2da7f3cb7095c85efb","datavalue":{"value":{"entity-type":"item","numeric-id":801667,"id":"Q801667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$F7FD799D-9D41-4735-87F9-FDE46448E2EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8ea372caa817f188e4e943a4cbc2ab55cc9d12","datavalue":{"value":{"entity-type":"item","numeric-id":5549412,"id":"Q5549412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$7E20BB0B-67F9-4D77-8BDA-B479C1B0BB53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35f820e9c2b45f8f035a710ad26c0ff0e5c7ae48","datavalue":{"value":{"entity-type":"item","numeric-id":3221381,"id":"Q3221381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$8B2267E3-8779-47C1-898D-4D1D82C65CF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dc01a28b8e042eaee4713d2ffe90785f0ff058b","datavalue":{"value":{"entity-type":"item","numeric-id":1163361,"id":"Q1163361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$3777E980-C1A6-45DC-846A-92809BD09970","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f3813ab614a97a156330c623ed2e7bf909d45fa","datavalue":{"value":{"entity-type":"item","numeric-id":4105777,"id":"Q4105777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$3486817E-1BCD-4A33-AD69-E026DC94159B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9c583b65c7819a91d7f03c50f27e11283eee826","datavalue":{"value":{"entity-type":"item","numeric-id":3962973,"id":"Q3962973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$A36AA76D-C206-4279-8830-16C604619444","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad49d7555b1464bcbb06a6c2fd8083015d9a3baf","datavalue":{"value":{"entity-type":"item","numeric-id":911245,"id":"Q911245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$B0EFFDCD-0086-4E7A-9D27-AA3D22A3DF2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a70c1e34050dcd0b61ce5a07aebe8c29e58c7b21","datavalue":{"value":{"entity-type":"item","numeric-id":3964001,"id":"Q3964001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$716FBB6E-649F-4682-9881-601D2F78F928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01d1f0f5487f8c0ee42819e7149f6be853525c70","datavalue":{"value":{"entity-type":"item","numeric-id":4729318,"id":"Q4729318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$2F27E717-8748-4B6B-BF05-314414E65A88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9985cb63b41fe11a8ab06f52de08161e27acbb2c","datavalue":{"value":{"entity-type":"item","numeric-id":1166272,"id":"Q1166272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$CFB74D41-D8BB-42DD-B4D2-7D294C787154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e16f53aacdc2272655a20338ee20ff055417e6d","datavalue":{"value":{"entity-type":"item","numeric-id":3954805,"id":"Q3954805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$E1F52E98-06D3-4BEE-B090-963E96D415BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"893133b7b86a6ea8f7bda9829deaacd67f7e2f67","datavalue":{"value":{"entity-type":"item","numeric-id":1131834,"id":"Q1131834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1179807$F23E92B4-FF17-410E-AE54-42A1B7A9BE50","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"660b3719580fbe63dc866cdcce498cd70b924723","datavalue":{"value":{"entity-type":"item","numeric-id":1199928,"id":"Q1199928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c82b1a6f4e53d73b2f0a5513a1af0f33c843bc0a","datavalue":{"value":{"amount":"+0.7030434608459473","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1179807$265B4584-8FDC-467C-B07F-C90E724C4E1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ec2537dcea7490ca8d09c48004d99af17f31f3f","datavalue":{"value":{"entity-type":"item","numeric-id":1607227,"id":"Q1607227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b09b7efc3bcef1a41fcdf502d59dd5e359dde2fb","datavalue":{"value":{"amount":"+0.7024356126785278","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1179807$F165E86E-3DE3-46F4-9CF2-8F6A038E9425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95bfb10a42c959c87e1db81626dd4be3d7e85b2e","datavalue":{"value":{"entity-type":"item","numeric-id":5096383,"id":"Q5096383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"111dddf6307b477e9129df9889fdf604047eb27c","datavalue":{"value":{"amount":"+0.6970760226249695","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1179807$3F4140BE-B253-4BF9-BE6E-8612C6C13CF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"415711b1c09bf2c5ec2ec1158544de3686ef1fc8","datavalue":{"value":{"entity-type":"item","numeric-id":719243,"id":"Q719243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"737c020db01d4d297a0b8f5fbfc86870bd36d5f3","datavalue":{"value":{"amount":"+0.6945037841796875","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1179807$19C272F9-D8F0-44F1-8F10-11AB64639542","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Context induction: A proof principle for behavioural abstractions and algebraic implementations","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Context_induction:_A_proof_principle_for_behavioural_abstractions_and_algebraic_implementations"}}}}}