{"entities":{"Q1791187":{"pageid":1801929,"ns":120,"title":"Item:Q1791187","lastrevid":53218820,"modified":"2026-01-24T12:01:40Z","type":"item","id":"Q1791187","labels":{"en":{"language":"en","value":"A formally verified solver for homogeneous linear Diophantine equations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6946995"}},"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":"Q1791187$89D0A3FA-6A7F-4E7A-B837-03F5F35B6BD7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"af7e02ef29c66675c00dcbb7a6f4eb7014b7a60e","datavalue":{"value":{"text":"A formally verified solver for homogeneous linear Diophantine equations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1791187$0B067848-3766-4F98-8CB2-905ED7240EA4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c264a6d7e26a39e1c69aa76a8583fbb09aee78f5","datavalue":{"value":"10.1007/978-3-319-94821-8_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791187$DD3397A3-917C-4CFF-BC3A-851FA1D3E729","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"40256d99b4420733fb59f3ac0a5e3b6cd5e0fed4","datavalue":{"value":{"entity-type":"item","numeric-id":1791184,"id":"Q1791184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791187$0FDF4ABA-5D28-4667-90B9-6D8D2222827A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b4e8b8854a2f5f1838328c162624d112c179ee43","datavalue":{"value":{"entity-type":"item","numeric-id":1791185,"id":"Q1791185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791187$45A795B7-5C2F-49E3-BAE0-7D8B06C86485","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"76908a96dd9a93ab0d464108cd942f4efb1dbe42","datavalue":{"value":{"entity-type":"item","numeric-id":1791186,"id":"Q1791186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791187$2FF5198F-9077-4AD0-8DD3-5166C70775DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0653fc883593f9e70c5ddda3d1f1f752c0d0ffca","datavalue":{"value":{"entity-type":"item","numeric-id":530846,"id":"Q530846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791187$D1D2D24E-2D74-456D-BA27-D02ED30FBC93","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":"Q1791187$59038B2C-7290-4A08-A491-8CAEF50076E7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791187$B46784A4-72A1-42D7-B9C7-96F5AC21B911","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"67c45964bb1554d8a802bf9a29e50db9b1c5a363","datavalue":{"value":"11Y50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791187$ADF0CA4F-0609-4173-88E3-8E8A1A348C56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791187$12C91E6C-2660-4F5D-A8D2-5259E9EB19D4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"506fbb9dfa4b503abd0214b095884aa9186e804c","datavalue":{"value":"6946995","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791187$00B2C76F-29E0-45E9-A046-7B879BF324DB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c2d4630e5de645038947bd96e9d4ac53e0adc93","datavalue":{"value":"homogeneous linear Diophantine equations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791187$690CCE58-3F6C-4C85-A8F4-BC0F77683F51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6bc6768f771e8ae47ba1683cf1d33a808061abb","datavalue":{"value":"code generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791187$B5A8E662-BE90-4D17-996E-89120348C475","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cc5cc8e8184b14b39b555e2997003bf3622dcaf3","datavalue":{"value":"mechanized mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791187$218DAB99-CD07-4771-9934-4DACC6385E49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8571af01308627f1225f1ce546463ee80f7f45b9","datavalue":{"value":"verified code","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791187$287C5841-21A8-4116-8C2B-2F2576AAE032","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791187$EC387B7B-5BC9-4DF8-8ECC-F0165D7326EF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791187$74D4DB14-B971-4867-AB6A-716C132E3F8F","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":"Q1791187$29F6535A-A65E-4909-B9CF-A9162BF3F6A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4aae8754d8245457dd720bfe48b4a61fd331666","datavalue":{"value":{"entity-type":"item","numeric-id":25547,"id":"Q25547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791187$A09D2629-E1AF-477E-81B3-9EF986A70027","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":"Q1791187$7F8E220E-8985-4881-BD69-DD27FEA94015","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"78b7abe32ca42d8511ad7deee449dba3cfaf53b0","datavalue":{"value":"https://doi.org/10.1007/978-3-319-94821-8_26","type":"string"},"datatype":"url"},"type":"statement","id":"Q1791187$3104AF65-D140-4B8D-99CC-247F785DC099","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b58e55f5a7bd212f5870027055fb58b1717d311b","datavalue":{"value":"W2810744507","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791187$3BABA77E-B06D-415B-8731-E7B9AAA54661","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e95706b86adb6f9693edbee0db1fd8fe26e83786","datavalue":{"value":{"entity-type":"item","numeric-id":1099648,"id":"Q1099648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f3679b5a6303762b08218e7b07927b9e5953094f","datavalue":{"value":{"amount":"+0.7645512819290161","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":"Q1791187$C4DD3773-52FA-4AEA-844D-2BA14AACBE55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"215137121412e0b1f51567744bea8f32970209cf","datavalue":{"value":{"entity-type":"item","numeric-id":5096305,"id":"Q5096305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bff79e62ad4820746fa75326948bdd8db73159e3","datavalue":{"value":{"amount":"+0.764371931552887","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":"Q1791187$9628E29E-4435-441D-81EF-DC16BEA5F8E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a15a4817023bf3bc7b69da94d013b6f29b9d70e","datavalue":{"value":{"entity-type":"item","numeric-id":3338216,"id":"Q3338216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3521fd43906b3b335827bd00a30b9121d3654ccf","datavalue":{"value":{"amount":"+0.7475898861885071","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":"Q1791187$7977629F-C682-425C-8AAE-C4A5ADED443D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"449016d82a18f729fff77be0c6f6c6787983951a","datavalue":{"value":{"entity-type":"item","numeric-id":1098653,"id":"Q1098653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25439d08eb2d09798010b77eb9cfc7893c62427e","datavalue":{"value":{"amount":"+0.7357019782066345","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":"Q1791187$9C8ED946-DF01-4559-B42D-B89182F558BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94a3013126c88788e1f2abca5dc5b703dde202bb","datavalue":{"value":{"entity-type":"item","numeric-id":3805960,"id":"Q3805960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f728f99a05d16625be11b6520b46c487a7f0318","datavalue":{"value":{"amount":"+0.7310813069343567","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":"Q1791187$36B5AA2F-8537-40AA-A885-0EB31D5D98B1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1791187","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1791187"}}}}}