{"entities":{"Q5875447":{"pageid":7904998,"ns":120,"title":"Item:Q5875447","lastrevid":39654645,"modified":"2024-12-30T16:43:27Z","type":"item","id":"Q5875447","labels":{"en":{"language":"en","value":"The DPRM Theorem in Isabelle (Short Paper)."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649982"}},"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":"Q5875447$0BDDF7CC-570C-4B55-992E-746F85BA8CA7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9ed986d16faf29dfe7dc6c5f3f78de89f11ffaa0","datavalue":{"value":{"entity-type":"item","numeric-id":2287891,"id":"Q2287891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$1443C5EF-D11C-4DD4-8C5C-0BD2D44BA41E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"42b861e3cfc1f930c29a2bedb324b3e645d29546","datavalue":{"value":{"entity-type":"item","numeric-id":2287892,"id":"Q2287892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$B3DEA58D-8E54-4832-9A2F-554E66BBB51C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"30529b2f926af91d7279ff430a09707209fc1ec4","datavalue":{"value":{"entity-type":"item","numeric-id":2287893,"id":"Q2287893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$63B050B2-ED63-420B-9E18-F94C27CDAC95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4c5d696d8f1e1ce09141ba564649132e50d8af7f","datavalue":{"value":{"entity-type":"item","numeric-id":2287894,"id":"Q2287894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$EC43BDE2-F309-49B6-9190-712F51CAF4A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c76c0a89551dbf0b0f8fb38cedb6841e51a3fe53","datavalue":{"value":{"entity-type":"item","numeric-id":218962,"id":"Q218962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$44B220FD-D764-4D3A-9541-4690FCABDFAB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5875447$C66145F6-DC99-47D2-9F14-2262C43135EF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875447$08EDBE1C-5CCA-488A-921A-A470B1C44DEB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f6571f5ac2c8ffef458b45968694dea8730e565c","datavalue":{"value":"7649982","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875447$69704818-12B8-4D50-A1F6-498F9C4B8960","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bff659492fac3e5bf67a394ac3a48a1c9b49ea1a","datavalue":{"value":"DPRM theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875447$12BA210C-4131-4E2E-B34C-19A5BCD51E42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"16852d397daf2bbcaad561fcfc45e655fe8e884c","datavalue":{"value":"Hilbert's tenth problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875447$74A2562F-B5C1-4DA5-8604-DB8101BC6C22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bdfdfca5ddda6f6b12ae7cdd184cf83d18716a6","datavalue":{"value":"Diophantine predicates","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875447$6D5D0A08-9922-4B71-9133-857B68D846C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7928c1c3157011dec56fb4f8a8cd86d60ac43236","datavalue":{"value":"register machines","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875447$FCBC2EDE-AB4F-45A6-9C2E-70289DD85A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bb5e53e93edfb5e939667dfe247041de4aa4ea85","datavalue":{"value":"recursively enumerable sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875447$4629D9C7-9460-4186-896B-47920520D8E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875447$0AC42BD9-2BC4-4E55-AC4A-D7BE17A2EFEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875447$B05FCB79-30F3-4661-9C14-E9F4F7948367","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":"Q5875447$A2ECAD28-871D-47ED-AC11-51884C22532B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"838aa8b13d97f90ffa4301f31c63b5795a784147","datavalue":{"value":"https://doi.org/10.4230/LIPIcs.ITP.2019.33","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875447$32116CC6-0E20-427A-98F7-F3737814A721","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4fa21748cd6e8950b75659ca7db2d0d9dbb20be1","datavalue":{"value":"W2978388349","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875447$87DEA1BE-70CE-41B2-B50C-4F7DEA0988EF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3600fd23fdc12a3f535852890696e7179d637c56","datavalue":{"value":{"text":"The DPRM Theorem in Isabelle (Short Paper).","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5875447$3B35DC2B-359A-44C4-B8A9-801C71AFB6C1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d5fbb4a3d0742b1066a736fa365548256665c05","datavalue":{"value":{"entity-type":"item","numeric-id":2287895,"id":"Q2287895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$F4097A07-BCA2-467A-ABC1-903CD2FD31B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db0194aac5d1b5fafc5d3a8db70fa2e0207b7ebb","datavalue":{"value":{"entity-type":"item","numeric-id":2715528,"id":"Q2715528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$E371A4E8-731B-4B19-88D7-0EAB4C16ACD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"466133b65efd4969cf0b67c8710462f853a29056","datavalue":{"value":{"entity-type":"item","numeric-id":2337340,"id":"Q2337340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$350977F6-2873-497C-BBED-60D5CEB3667D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c02baa06229f9c8e47415ba00fdd6dfa7fc577b","datavalue":{"value":{"entity-type":"item","numeric-id":5327342,"id":"Q5327342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875447$60C5F946-DD34-4BAE-A2BF-6BAE848E7841","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6832f7010925fcccf780fa9f8ae19d8669cf594e","datavalue":{"value":"10.4230/LIPICS.ITP.2019.33","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875447$2D083047-B59D-4F8E-BC68-81D715F45164","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5875447","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5875447"}}}}}