{"entities":{"Q1714805":{"pageid":1725546,"ns":120,"title":"Item:Q1714805","lastrevid":70804764,"modified":"2026-04-13T17:19:41Z","type":"item","id":"Q1714805","labels":{"en":{"language":"en","value":"Formal proof of a machine closed theorem in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7010789"}},"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":"Q1714805$9B80C8AB-F258-4C53-A073-84F440102528","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4cf5d8668eaefd9c2ebbe26219f81589ad933022","datavalue":{"value":{"text":"Formal proof of a machine closed theorem in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1714805$A208DC75-F55C-4D8B-B03B-CEE029A233CF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"91e2285b435b21df71b1814328aba5119865cedd","datavalue":{"value":"1405.68316","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1714805$7F514A9E-8CAE-4E98-9E9B-C9C7E84BE8FB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"de7fb27beb0888eae5f3219eed4e27161f76ef1b","datavalue":{"value":"10.1155/2014/892832","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1714805$13E16B5E-DDB5-4BC2-85A3-EF066ED62C41","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"442ab4f251eef23225015c1082eab0d1a65dcdaa","datavalue":{"value":{"entity-type":"item","numeric-id":646091,"id":"Q646091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1714805$796C7636-F0BF-4C36-A311-3100EDAC462E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3ccb57183c53f576df777f62c0ab9a5920ef22fb","datavalue":{"value":{"entity-type":"item","numeric-id":636561,"id":"Q636561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1714805$59639258-74A7-44EF-A938-B9A0CF3A06F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57ce671c876a01ae9569e5abc7a9678694bba6b0","datavalue":{"value":{"entity-type":"item","numeric-id":646089,"id":"Q646089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1714805$7908327A-5997-4590-B0BE-D81E63C3A366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"38174302f60e3d3833be48f48a067ba5fd1aa08a","datavalue":{"value":{"entity-type":"item","numeric-id":646090,"id":"Q646090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1714805$540A3956-EF89-4DF9-B91B-B9336336F772","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1714805$95175981-4796-469C-B501-51DF2E9A04F1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3f4145805478faad59761c3ff4a8cc3fff513172","datavalue":{"value":{"time":"+2019-02-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1714805$05B884AC-926B-4DF4-BEBF-D57DBD771080","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"35f34de7a9b2f62a42dbd4a52df6747ea9c06f8d","datavalue":{"value":"Summary: The paper presents a formal proof of a machine closed theorem of \\(\\mathrm{TLA}^{+}\\) in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform. A useful proof pattern of constructing a trace with desired properties is devised. A number of Coq reusable libraries are established.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1714805$CB05BA4A-6F8C-4AE7-8318-825544BEC152","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1714805$AE61D76F-8A2F-49DE-A876-17B7B179AFC0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"16b43c8cbb74c2592a677cc7e454111f92589b6f","datavalue":{"value":"7010789","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1714805$CAC6B379-D7F9-4C0B-B4BE-DFE1416E1948","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"961ee19419087c06b287d462986b729a8fbf11af","datavalue":{"value":"Q59054162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1714805$F1EF9444-70D1-4251-B1F6-DE6E9639E04B","rank":"normal"}],"P1463":[{"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":"Q1714805$C0D8166B-6BC1-40D9-A729-78A0F04D7E22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1714805$2A3F598E-1DEE-41C3-A595-BD245B577EC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1714805$2DECD0A6-1369-420C-8AEE-DC1578B7DC4A","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":"Q1714805$F2F1FDD8-D1C8-4ECA-8717-0968B1EB80CA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"feb341a5c7d14e1428fb2d830c6a305af6ea5b08","datavalue":{"value":"https://doi.org/10.1155/2014/892832","type":"string"},"datatype":"url"},"type":"statement","id":"Q1714805$E7338604-4934-49E0-968B-D9786CCCAA4F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6bf0c98c85ee9b0fbfe8fab211d72e8104a7c895","datavalue":{"value":"W2017200838","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1714805$C9D63632-5992-47A8-BB5C-5C237D7589FE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be6750cd750a678c63f2278474a446b88f4518bb","datavalue":{"value":{"entity-type":"item","numeric-id":5327343,"id":"Q5327343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e522861a7709cc5d501f5f3bd91091f969b8f3b9","datavalue":{"value":{"amount":"+0.7169661521911621","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":"Q1714805$330303E8-FE90-42E9-A6FD-4B1C8D017419","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c1cb744e836204235a33b303d4115c8b81e3aa4","datavalue":{"value":{"entity-type":"item","numeric-id":2754058,"id":"Q2754058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50aa45671b92ca76340ac45dc0e694a8ccba19b7","datavalue":{"value":{"amount":"+0.7097293734550476","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":"Q1714805$2B2B6B63-7FD1-4941-9B82-CAB1184D8FE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eb9707e33700967679010ac1d47d134b3b741111","datavalue":{"value":{"entity-type":"item","numeric-id":2879241,"id":"Q2879241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccc1da60b0cf43f7a6679ca50795bef0f81b1be8","datavalue":{"value":{"amount":"+0.7067534923553467","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":"Q1714805$FD2D2F01-76A3-48DD-B484-5E2D15D49BB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f5338f7ed3775f2c4b0a5afeaf8ce6094c68557","datavalue":{"value":{"entity-type":"item","numeric-id":3024875,"id":"Q3024875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a95b62904f49c53a76daf6a24458adba217a7c3c","datavalue":{"value":{"amount":"+0.7044129371643066","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":"Q1714805$7C94E28B-DCC1-411A-80EF-C99AC1926E22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"383293963e7c1b01bd5a14b4cc3c73537c26a169","datavalue":{"value":{"entity-type":"item","numeric-id":4647839,"id":"Q4647839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"934fa9a9025861c46f3e774d92083b9d638c1454","datavalue":{"value":{"amount":"+0.7000508308410645","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":"Q1714805$61D66129-40F3-4D4D-8D9D-43A12424AA19","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal proof of a machine closed theorem in Coq","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_proof_of_a_machine_closed_theorem_in_Coq"}}}}}