{"entities":{"Q2955752":{"pageid":2966472,"ns":120,"title":"Item:Q2955752","lastrevid":56790690,"modified":"2026-03-23T15:00:35Z","type":"item","id":"Q2955752","labels":{"en":{"language":"en","value":"Tactics for mechanized reasoning: a commentary on Milner (1984) \u2018The use of machines to assist in rigorous proof\u2019"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6674700"}},"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":"Q2955752$B09460DE-1CE9-4B13-8DC4-CD372481B966","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ae3ae961578c4b6f378b08b8d523152a39d50d7b","datavalue":{"value":{"text":"Tactics for mechanized reasoning: a commentary on Milner (1984) \u2018The use of machines to assist in rigorous proof\u2019","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2955752$4A4D241B-8131-497A-8DA4-A2235C8B3986","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1a9955fd8f781ffe452b4eddb87c4e4a160ae10e","datavalue":{"value":"1353.68250","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$EB97BDF8-33D1-4B40-8B8F-514A23F339BC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"931e30a40c8472ba029c509504f463b9cccdfd3d","datavalue":{"value":{"entity-type":"item","numeric-id":436371,"id":"Q436371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$E10A5236-624F-4BA8-B85E-F9B1CCCAFC21","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a13ffa206096651a7eda5901a1abc51007a10be2","datavalue":{"value":{"entity-type":"item","numeric-id":144519,"id":"Q144519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$9B2086AB-0828-4DC6-9F18-611C2CA45017","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"583d34ca42387c838863e913f9ffa1c8da88851c","datavalue":{"value":{"time":"+2017-01-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":"Q2955752$5C2AAF67-C642-4976-B6D4-33937D7684E0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$EEF09E1C-5FFA-4342-A8D1-841DED94D9AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"540259e42205310d3310d3dad9dbe9ae50303b84","datavalue":{"value":"68-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$EB4B5B4F-6B92-44DB-A80D-550877C59BF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"855dfff3c52593115343606bc2418a3b17e5a003","datavalue":{"value":"01A60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$B71E7AE9-DAC8-48C0-90C5-C67AB1874018","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d1e4be73bf513c2eaaaafc3e2477b6f09dbbd551","datavalue":{"value":"6674700","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$61AE90F1-72C9-4983-AA03-85948539AEF8","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":"Q2955752$2D8CCB0B-8EC6-4ADC-8740-638B286FF040","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0fba089b3d5f9abc32e01aa45331c891d75b080d","datavalue":{"value":"https://doi.org/10.1098/rsta.2014.0234","type":"string"},"datatype":"url"},"type":"statement","id":"Q2955752$EE8C4A98-48A9-438F-94AC-D3A6184A9DDE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1da290f8ddda43ce326c99e98cd05f21c976aefa","datavalue":{"value":"W2077244951","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$B6FD6276-412D-4511-805F-3DCB592F9137","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"54d7036a20fc54b777b10eca1e0c61ddf8fd0948","datavalue":{"value":"Q41871292","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$5F091B3C-EE6B-4478-8D57-733AA779C092","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$AD85E983-0E07-4400-91DD-D3B6B77504E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$AFE9FEF6-88BB-425F-B337-26031E87B425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d00685e690962496b9171a3355f96696227f14ef","datavalue":{"value":{"entity-type":"item","numeric-id":5528159,"id":"Q5528159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$2BB41DC2-82A6-4683-B970-2E90D1AD6BD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d4ddccf9258c9f31fa193f202f774ffec18b8","datavalue":{"value":{"entity-type":"item","numeric-id":1250704,"id":"Q1250704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$D3D1E0F0-718F-40D5-9E78-5811AE67245B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c980747852309ad02e34011dae7b1195dd483e00","datavalue":{"value":{"entity-type":"item","numeric-id":3690258,"id":"Q3690258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$10A793D0-E24D-4ACD-B6E1-E38FA3AE007B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"527c7202e783b352edb1e0158278fe604f9a2b5a","datavalue":{"value":{"entity-type":"item","numeric-id":4105761,"id":"Q4105761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$378ABDD7-E33E-4F18-A51D-8FA421C34909","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c05aa45210aebb87236e38d8954563df144e4d","datavalue":{"value":{"entity-type":"item","numeric-id":2940885,"id":"Q2940885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$4561F25D-C4FA-4E8E-AD86-9382EB6EE122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef9ffe7c2da508307634101c6c88ac8cd76fa38f","datavalue":{"value":{"entity-type":"item","numeric-id":540690,"id":"Q540690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2955752$844B8EC3-E840-4215-B3AD-415A3FDB926B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7a4f7ff4bd99343c1ff8708b22bd7006e790fb27","datavalue":{"value":"10.1098/RSTA.2014.0234","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2955752$D1282DBE-405B-4B11-9915-8EBB98B6A123","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":"Q2955752$CF16AF0A-3827-4535-A763-B8C9D521A006","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2955752","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2955752"}}}}}