{"entities":{"Q2575736":{"pageid":2586479,"ns":120,"title":"Item:Q2575736","lastrevid":48606685,"modified":"2026-01-05T08:59:53Z","type":"item","id":"Q2575736","labels":{"en":{"language":"en","value":"An interpolating theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2235823"}},"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":"Q2575736$96AB3739-0822-4454-BC80-A89136419601","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fad7792047c8613b7517be9fea26d5d16f0e06c1","datavalue":{"value":{"text":"An interpolating theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2575736$31B6B1E9-8DD2-4E2A-A72A-8AA9B25C64B4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"89cad8d5af313ef46921a9cd54a8a35d9707e48f","datavalue":{"value":"1079.68092","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$3D368711-4647-4CEC-B8B0-D05420D30DCB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$0332FBF3-3703-4BC1-92AD-08B246DB0014","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b09223eb41f2578445149fa9e31b1db1d112f337","datavalue":{"value":{"time":"+2005-12-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2575736$9B15EC3B-49B6-439B-AAD4-A275F5EE08CF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$7663563C-3104-4186-B4B9-0039016466D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$DB3BCCBF-3419-4E9E-BA8A-8D7B6D790855","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c1d2d83da0d870574277144fdd1db9abaae162ec","datavalue":{"value":"03C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$D818578A-4D4F-43F8-933C-2E367ADF4DA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$DCA33A99-2976-4BEF-BEAF-8FE4DD637826","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e593c7ccb338293a03413fd4123626bb9988f5fd","datavalue":{"value":"2235823","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$4A9CA5BF-3136-45A8-860C-301A1FC3B8EF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03f1ce721ffa5b2f36084f57048f17032077e128","datavalue":{"value":"Craig interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2575736$6A786B61-2390-4533-8248-1862F02B8F85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5541349f29c25ba6a0be12f614381c30b7057b17","datavalue":{"value":"Model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2575736$0EAEF70D-3282-428F-A852-65FD0889A0FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"20a1d8b3158c8e54d3eb6dc847ad8b1b709f4bfa","datavalue":{"value":"Decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2575736$525955D4-B79D-4ADA-A450-C6ECDD172883","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f59730cf7818c892312636bed117bd3460e24595","datavalue":{"value":"Infinite-state systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q2575736$1FF01E51-C0B3-4607-9EAD-B525DF6C46E9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"57a84b3343ed70002617a9eb1439c18c15bac9ff","datavalue":{"value":{"entity-type":"item","numeric-id":934708,"id":"Q934708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$10A919A6-B138-4D98-896D-0F5F03DB33F4","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$E66D9E3F-FF89-48AB-826A-6225A9C6CD64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3fa0ba30f2225a69a75d233361703cec68c39010","datavalue":{"value":{"entity-type":"item","numeric-id":15473,"id":"Q15473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$2707CE2E-C443-49F4-A240-8909DAF66DF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6c46d83f8225e8e4d789b6fc74144d78a1809470","datavalue":{"value":{"entity-type":"item","numeric-id":24792,"id":"Q24792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$A8EBB30F-913A-422F-AB65-217E8D4F92D6","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":"Q2575736$7D477263-77D6-4C9F-A7B3-87F7156D979B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8c2de178f67bae0749f2dcd18196c9ef4e205ecf","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2005.07.003","type":"string"},"datatype":"url"},"type":"statement","id":"Q2575736$F5710301-2FB4-445F-B902-A0618230A930","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5291bd6baee73239027292f78ea2a85589e1d4e3","datavalue":{"value":"W2084294613","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$43845A6B-5AA5-4CA8-ABF5-BF378044562E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf4fab5a4519bb0e4a7392865538dc50ad77fca2","datavalue":{"value":{"entity-type":"item","numeric-id":1193587,"id":"Q1193587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$374B2A48-4EE3-4390-898D-B044ECA21098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7de140db476e3cb4a77792caeebac28e6bb14357","datavalue":{"value":{"entity-type":"item","numeric-id":3244103,"id":"Q3244103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$A2B9D2A5-570C-43F9-A917-A1A74DC3B74F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6da6ded218db8e1aba2fc38982f0c41333c8292d","datavalue":{"value":{"entity-type":"item","numeric-id":4809077,"id":"Q4809077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$8EA6A018-CD57-4301-8A34-4AA2CFAFDE15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4e94238a6a5ddf3dd15f03313efac1f027d9611","datavalue":{"value":{"entity-type":"item","numeric-id":3452263,"id":"Q3452263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$17CECF60-2672-4D6C-92EB-377F2E6156B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30b9e272f8ccce6a7b10c8e4afc506dcafb4f348","datavalue":{"value":{"entity-type":"item","numeric-id":4358049,"id":"Q4358049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$4B3674FB-5D4D-4EAB-96D0-E7B02FB93C20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15f2de53b1bf73e880cd8935ca36395fbd675bcf","datavalue":{"value":{"entity-type":"item","numeric-id":5900675,"id":"Q5900675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$1FDC49B3-A95D-498C-8D88-6F83D113478A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"348369ca3fccbe91226809a75cbf31afd7f3186d","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$B672F958-5027-410F-8A59-A9BA1D5C2453","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7ee42bcb5651ff1d6441d36735f61656172044f","datavalue":{"value":{"entity-type":"item","numeric-id":4417909,"id":"Q4417909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$72CB892D-150C-4660-8318-1762CADFF88B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$F1B047C8-BB5A-4B3A-BBAA-8CCBEFFA06B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"008723b33cb14bbda59226503d753d137dc6f8ef","datavalue":{"value":{"entity-type":"item","numeric-id":1098330,"id":"Q1098330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$354BA851-59F6-48ED-B7BB-C7B8E9F75F31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40f34823cac176489a74f3e54ebb7fe9577d93ab","datavalue":{"value":{"entity-type":"item","numeric-id":4372917,"id":"Q4372917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$A7B989CA-E5C7-49C5-8FE1-2C32940FEC1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9269e64d2adca53bb2f298ca1a02b550d98c27a7","datavalue":{"value":{"entity-type":"item","numeric-id":4571400,"id":"Q4571400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2575736$112A7CFC-D821-4392-B5A3-2E0D2D67BACE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"55d8a14a874a671b0c5e88963e36babf63262841","datavalue":{"value":"10.1016/J.TCS.2005.07.003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2575736$6B5E4350-AE2D-4760-97CE-0466D3DCE814","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"192babe1f332f85d504aff10a4562aaa3e265788","datavalue":{"value":{"entity-type":"item","numeric-id":5308386,"id":"Q5308386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"612e66f6c64215cdfbf23516093f5455602049ea","datavalue":{"value":{"amount":"+0.9987240433692932","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":"Q2575736$2659C6CD-367B-437E-9650-04A7F16A3980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb253fb55714f511287e3fb7db3bf54cfc2f7066","datavalue":{"value":{"entity-type":"item","numeric-id":5311270,"id":"Q5311270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ca912a7773d35c7cf5a427ce056eb7aa07870ac5","datavalue":{"value":{"amount":"+0.8679428100585938","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":"Q2575736$42E0BF7B-D511-4B63-8511-DA14863C9CD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9431cbab61d866d4fa0af21733b3d4eefd8fc797","datavalue":{"value":{"entity-type":"item","numeric-id":5747778,"id":"Q5747778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8157b40d597717f52075c6f9261e9ac3dc4789ec","datavalue":{"value":{"amount":"+0.8305278420448303","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":"Q2575736$849D6CF6-5C7A-4A3F-89D1-0391D0D96057","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6082005cb838151ec2f536065030af8f23f991cc","datavalue":{"value":{"entity-type":"item","numeric-id":5452599,"id":"Q5452599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b3f151a2a4de4f3a7855cda214e5209227dfd3f","datavalue":{"value":{"amount":"+0.8264830112457275","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":"Q2575736$4F28D619-1EAD-45E3-8D02-715BD6A5DE71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5302c862f26649c1cb13bd6e9bc82d762cb6ba77","datavalue":{"value":{"entity-type":"item","numeric-id":604394,"id":"Q604394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c720991d7a2b9040e6ead9b87b4371239c02ff9","datavalue":{"value":{"amount":"+0.82572340965271","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":"Q2575736$39E3AEE7-DF25-4374-9C62-2AE516466CB8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2575736","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2575736"}}}}}