{"entities":{"Q1791179":{"pageid":1801921,"ns":120,"title":"Item:Q1791179","lastrevid":72966561,"modified":"2026-04-14T09:04:37Z","type":"item","id":"Q1791179","labels":{"en":{"language":"en","value":"Proof pearl: constructive extraction of cycle finding algorithms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6946991"}},"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":"Q1791179$BC99EFB7-235B-4A05-965F-D8EDA9A056A8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5f8f9a7c201c366d4e740cd113f9d40c01b87576","datavalue":{"value":{"text":"Proof pearl: constructive extraction of cycle finding algorithms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1791179$A20A30D0-564C-409B-A3C7-46FF5961D3A6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"61317edb39028dce9a38f0d313a3532164dc4a4a","datavalue":{"value":"10.1007/978-3-319-94821-8_22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791179$390CD0FE-B5E2-4202-8EA8-791D51A462DF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa467ab0fb5921a8aef55b984db7a2882bc4957f","datavalue":{"value":{"entity-type":"item","numeric-id":877885,"id":"Q877885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791179$B38B9DD7-8106-4939-83BC-B51D71B82137","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ff3c7136492fcf13c84b92efb7ac37b3eed57322","datavalue":{"value":{"time":"+2018-10-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1791179$1BBE9813-DBCE-49BC-97E4-379C71946289","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791179$1F9565DE-F534-4763-BE48-34683821364B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a5e47548ef139717b317f83801cfef606a623d","datavalue":{"value":"05C38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791179$4F0DE07E-8C35-420B-9BA1-683E90654950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"749b7137f279a66a306e75e15f613231b281c1c5","datavalue":{"value":"05C85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791179$4BE8174E-ECFD-494C-BBB3-9ED1ECF68B62","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cc8166996b5a533ebfedd75097a990b1d7f1ff7c","datavalue":{"value":"6946991","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791179$C455CD72-1BA5-4EBD-823D-A83401ED48EB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83b7c8409e02c8e81bea013d23ff3f9277d4f9c4","datavalue":{"value":"cycle finding","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791179$8D13931A-B4D5-440D-82DC-6ABA52168D6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b31d9966037df112e4dce8cb92900aece35a40c1","datavalue":{"value":"bar inductive predicates","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791179$1DA9CC4D-4192-4FDD-B39E-75C5ABAF8F07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03fa8a7a83c058915d902ef385fa299922554764","datavalue":{"value":"partial algorithms in Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791179$30DC03C2-36D3-46AC-9615-F110A6B4D375","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6e70b6a8b856a0284222ee9895119f431a960b13","datavalue":{"value":"correctness by extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791179$FF86DB1F-3AB5-4848-929D-F2C19B60037E","rank":"normal"}],"P1463":[{"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":"Q1791179$3E046C73-FFBF-43EF-BF16-6731A50BA75B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791179$3CDFB181-AFF5-4717-96BB-826CDB1E1356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a6f53b82088d860910a0e22e3ebcf5898419a42b","datavalue":{"value":{"entity-type":"item","numeric-id":40364,"id":"Q40364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791179$1EAD5910-5BC2-48C5-B93B-404D77DBB9E4","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":"Q1791179$B9867FE0-201D-48FF-A75D-59BC97E20EDC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4bc0baeae0dcf1e79176e70476d10fd210fe80be","datavalue":{"value":"https://doi.org/10.1007/978-3-319-94821-8_22","type":"string"},"datatype":"url"},"type":"statement","id":"Q1791179$8E68D99E-718E-4DA4-B315-83401664038A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"83cc0d6718eb17ecbd2d53ededbc60c780087c37","datavalue":{"value":"W2810357523","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791179$40943F79-01CC-4925-8EAF-2FB97F5D965B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"31e06b4fe6c983bb3ab4de626b40fdcb19de88e0","datavalue":{"value":{"entity-type":"item","numeric-id":1823656,"id":"Q1823656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5aa43d044bbd32a8d55627ffab665b040d1fbfb5","datavalue":{"value":{"amount":"+0.734533429145813","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":"Q1791179$EF8376F7-3043-4A2C-90CB-A1317608E8C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a49efe1002fe0ae12dff09a0d1de418844a82427","datavalue":{"value":{"entity-type":"item","numeric-id":4460836,"id":"Q4460836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cdf4983ae035945688fb55a50433fc4db1d1743","datavalue":{"value":{"amount":"+0.7215684652328491","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":"Q1791179$DD1CB56D-069E-40CF-95AF-338DF8034E3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e685d69d283656beb9594427f4c97f9ccfa7280","datavalue":{"value":{"entity-type":"item","numeric-id":4421868,"id":"Q4421868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb03708146bb3698f220979c1e1665e074c5eab2","datavalue":{"value":{"amount":"+0.7119165062904358","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":"Q1791179$F0BAD3A2-C7FB-4F3F-B486-9820A1178A97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65e3d3670795b31d38c0853f7f79ca71b1eda741","datavalue":{"value":{"entity-type":"item","numeric-id":2703717,"id":"Q2703717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb03708146bb3698f220979c1e1665e074c5eab2","datavalue":{"value":{"amount":"+0.7119165062904358","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":"Q1791179$0D99D2F5-6C73-4B77-A23A-E46AA717E1E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75cfc7d997c33ab783a0f8b7577b99fbfdcdaeea","datavalue":{"value":{"entity-type":"item","numeric-id":1595930,"id":"Q1595930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"41611cd7bd5557c899660179c9f19d4756548179","datavalue":{"value":{"amount":"+0.711042046546936","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":"Q1791179$E63CBE7E-53BC-4534-B647-57858FD0D7DF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof pearl: constructive extraction of cycle finding algorithms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_pearl:_constructive_extraction_of_cycle_finding_algorithms"}}}}}