{"entities":{"Q667526":{"pageid":669375,"ns":120,"title":"Item:Q667526","lastrevid":63412026,"modified":"2026-04-11T12:48:17Z","type":"item","id":"Q667526","labels":{"en":{"language":"en","value":"Automating Event-B invariant proofs by rippling and proof patching"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7035357"}},"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":"Q667526$BC7BFAD8-C048-428D-B338-DECD441B7324","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bad431fcbb15a184e41f9058172bc43f3574364f","datavalue":{"value":{"text":"Automating Event-B invariant proofs by rippling and proof patching","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q667526$DD8F2C70-0AB7-4878-A37B-5600DF2E321A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b7ce851ba5eae0a5e75ffa4c4b1f98bbe0882cb5","datavalue":{"value":"1425.68077","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$746B58A7-E083-4851-B5CA-10A8880E4AAF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d37a3d6bd9a0b44736f3bc6a6985f44383a95724","datavalue":{"value":{"entity-type":"item","numeric-id":438542,"id":"Q438542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$EF7D2329-9015-4C05-B2D2-AE5C42188768","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"51b90353512d814f6655789de8fa8f4adf362ca9","datavalue":{"value":{"entity-type":"item","numeric-id":656857,"id":"Q656857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$F392EA8D-E922-4AB0-AAC4-BBF3358CCCD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"39eefdf43007a5db029de99b1444c96ff88fcb4b","datavalue":{"value":{"entity-type":"item","numeric-id":667525,"id":"Q667525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$0273E73A-FE7D-45C5-9353-37498BF07E70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6aa3d86338918dee908958b5264a955742f73846","datavalue":{"value":{"entity-type":"item","numeric-id":301484,"id":"Q301484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$16B2B119-E897-4D33-97A5-75E7148BB3AB","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":"Q667526$443A1C64-9D6E-4089-959A-A656F7A82660","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b783351c35e120ec0bb7c5359bc3eabb3a21294c","datavalue":{"value":{"time":"+2019-03-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q667526$9FB82F8B-B8FC-4335-8292-71DBE51E5427","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$23084240-A520-424D-8D57-1DF6C8AFFFC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$9524882E-5345-4B5C-8C2F-DA58D2B1E6F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$89006489-F875-4A19-9F56-5BDF3395FE2A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"94232b802aa85b7e323829a570a597666c402274","datavalue":{"value":"7035357","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$26FE7614-0B48-4688-AC01-C996D26D5F22","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q667526$F4083852-882C-4980-8964-0B0935006EDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"04ba4bf98dd124c8c2742b84b6fb188b54821857","datavalue":{"value":"Event-B","type":"string"},"datatype":"string"},"type":"statement","id":"Q667526$973170F0-B835-4C38-AB2B-9708D1104744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q667526$E1242287-F7F7-4C91-BC3B-5EC973E8255B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dcd23f1ac15738884d4f597ff06d742c7a60a96","datavalue":{"value":"rippling","type":"string"},"datatype":"string"},"type":"statement","id":"Q667526$D5A4FA54-3446-4D2E-8C04-1DCC7F89D976","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"306dab216dca5e2ff389f3aa1e0883c1f0a69eae","datavalue":{"value":"lemma conjecturing","type":"string"},"datatype":"string"},"type":"statement","id":"Q667526$1564E9E4-B538-4EE0-BD98-9B767490E395","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab1ccc8faeab7e6c417af9846c477f0e521ebe1b","datavalue":{"value":{"entity-type":"item","numeric-id":14592,"id":"Q14592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$D0EF3C2B-EE5C-4ED1-B7A9-940446D9A35C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3dcf6ea9ac65c890e0513ced8e4b0dde71e50b0f","datavalue":{"value":{"entity-type":"item","numeric-id":19141,"id":"Q19141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$27CE6EFC-D878-46B1-ADCA-5D1D38F36CFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3ef769e964c162d9fc2eb5be086cec28e8fe11d8","datavalue":{"value":{"entity-type":"item","numeric-id":5973367,"id":"Q5973367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$3D50AEC4-116D-40DF-B2AA-CCC3088BBCD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$9F382585-14F5-4522-926D-60480898F2BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8b2040a476017b43b21bd352cfec0a67d631d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":18467,"id":"Q18467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$EB3AF509-33BF-432A-B02F-E1699A7B6595","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"56183f18c1b7292025f517695163436751950f86","datavalue":{"value":{"entity-type":"item","numeric-id":22253,"id":"Q22253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$46E28472-5B3F-4AC1-9EB7-0DFF5A2FF251","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":"Q667526$93FFBCA3-C261-4323-BA43-2D5AC3FEC77A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"36c044034ac4476e6dc708b56bab7f38ea6a7d53","datavalue":{"value":"https://doi.org/10.1007/s00165-018-00476-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q667526$ADEB0313-6F73-46B3-866A-66F63CA44BED","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"adb2968358cb2c861d2629197a1c33769600c7af","datavalue":{"value":"W2908173533","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$81FB9906-23D3-41D8-AA8E-8C7691B291C7","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ba65bf6f54711cdbf437b6848150a44748b99faa","datavalue":{"value":"Q113906136","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$FF0D9022-3538-47C7-A039-4B4D5DC8F355","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae170f67b5a99f655b51707d2e6917e4913c4d7a","datavalue":{"value":{"entity-type":"item","numeric-id":4208552,"id":"Q4208552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$1C4207F0-F834-4EFD-9690-F83382938912","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a64dbb7c90690de5fbdf0d30d9b861ec41a32a6","datavalue":{"value":{"entity-type":"item","numeric-id":3569584,"id":"Q3569584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$575491AC-086C-4B14-9E9F-898EE46D5180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a42635e354ed5a90dff7abb6b01b6c7ff160dc","datavalue":{"value":{"entity-type":"item","numeric-id":5462949,"id":"Q5462949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$8982EE30-8951-42A3-BF70-4D4F6F45AA84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8cd4cda5b9483e9c53b052409071d90933892b9","datavalue":{"value":{"entity-type":"item","numeric-id":3838801,"id":"Q3838801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$F7AFA041-8C8B-40EB-88E2-90A905F493C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8955e894c8fbd524052b951c043bae4e14d12c6","datavalue":{"value":{"entity-type":"item","numeric-id":2870138,"id":"Q2870138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$E06F0228-69EB-4763-A9CD-7605A7FC5613","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c5239edfd305efbd1c9a075b6bf62b0b4959a45","datavalue":{"value":{"entity-type":"item","numeric-id":2870142,"id":"Q2870142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$709A6149-78F7-4AF8-A49F-F7AD4DBF59C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7db98659fd0d8d989353341e0c12c4246dfe6ee1","datavalue":{"value":{"entity-type":"item","numeric-id":1915134,"id":"Q1915134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$8D55F168-5CD4-4212-80B4-728A3B104D48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0f2d594f407efe37251ac80ff3ba201bad0e3a7","datavalue":{"value":{"entity-type":"item","numeric-id":1951639,"id":"Q1951639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$3ED7AE39-5BC1-4B20-8DB9-08FDE16C72CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc68d0c63fc526ea5871bf3910e143d716cf06f9","datavalue":{"value":{"entity-type":"item","numeric-id":438543,"id":"Q438543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$482327D6-507A-4D91-A44A-0AB1BEA06235","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a98e1d68003b0040c15c163e66f3fd9578fb9386","datavalue":{"value":{"entity-type":"item","numeric-id":3997074,"id":"Q3997074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$B0DE5DC9-C700-4099-B7AC-1752E7E1289C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0933abcee6e71217a619391222ae8646b0eea736","datavalue":{"value":{"entity-type":"item","numeric-id":5495917,"id":"Q5495917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$81E0673F-9E31-479D-B139-A6C82C7D06AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a4325e8f85fef0663ab4953d1e4cbc4c0595db","datavalue":{"value":{"entity-type":"item","numeric-id":3992808,"id":"Q3992808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$A9ED2E72-8E15-49D7-BA4E-BE3874D0BFCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$5D9E967D-5AE4-4E76-8CEF-98234CE24719","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc22454e59c42890989b223acb2a7da42f9239c9","datavalue":{"value":{"entity-type":"item","numeric-id":4301167,"id":"Q4301167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$23B5F574-97C0-433E-BECA-5CA2CEF8E476","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"504380b82096764eac291918951da560b52435b4","datavalue":{"value":"10.1007/S00165-018-00476-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q667526$EB96F866-0843-46E4-8D64-66D7823FB4D2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19f3d90aa73f3cee0039beefd5ac9443379c6629","datavalue":{"value":{"entity-type":"item","numeric-id":2165497,"id":"Q2165497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c4581958d53f0589e1c0eca307bb436fb979b7b9","datavalue":{"value":{"amount":"+0.6862793564796448","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":"Q667526$FFDEF510-C7E6-4AB4-BF6B-EAD40D14A967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b70983583bd7e5ea71011477dc85b183843e87af","datavalue":{"value":{"entity-type":"item","numeric-id":5464716,"id":"Q5464716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1a5d18bf67a0e9439c1087abedf07f2d141f282","datavalue":{"value":{"amount":"+0.6655920147895813","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":"Q667526$19C89AC2-72BD-426C-B445-43977B8F509A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1bf6b76195465b3a1366ac929fc1e8c3d4250488","datavalue":{"value":{"entity-type":"item","numeric-id":3066119,"id":"Q3066119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0da6014a81c4442690970d2713be79aa0b50ef7e","datavalue":{"value":{"amount":"+0.6641215682029724","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":"Q667526$75FF748E-D2AD-41CF-86B4-B8C9A360AECB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dc5e356a5e9f5403b0fd5200e4d64e9f97c50b4","datavalue":{"value":{"entity-type":"item","numeric-id":2994490,"id":"Q2994490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f1a94700b626c0cc6f34a8432e76a589198da00","datavalue":{"value":{"amount":"+0.6594480276107788","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":"Q667526$2A5D6214-5728-4414-8C14-612E7DC72F21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8ea74d8cc38401804b0f4418fa62cad1c586e70","datavalue":{"value":{"entity-type":"item","numeric-id":432154,"id":"Q432154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31bdbcd5d969bbb8bd984ed55f7f9f1d0a23b5e2","datavalue":{"value":{"amount":"+0.6571235656738281","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":"Q667526$306D3A87-B2D7-4CFD-986A-EE8275B94C7C","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q667526$CFCBDB80-A706-494B-A723-F105A33C3608","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automating Event-B invariant proofs by rippling and proof patching","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automating_Event-B_invariant_proofs_by_rippling_and_proof_patching"}}}}}