{"entities":{"Q7025191":{"pageid":21654045,"ns":120,"title":"Item:Q7025191","lastrevid":77543552,"modified":"2026-05-05T04:01:03Z","type":"item","id":"Q7025191","labels":{"en":{"language":"en","value":"VIRAS: conflict-driven quantifier elimination for integer-real arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7986590"}},"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":"Q7025191$894BDC44-40FE-4D75-906A-364FDDEB75E9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"66fbef4725f08083308b0c259ca2ee6b02137fbd","datavalue":{"value":{"text":"VIRAS: conflict-driven quantifier elimination for integer-real arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7025191$41C263E1-B2FB-4CFE-B1E4-14F45D65C8D4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fc8ae59c61850ef5b194d44f31a150967767680a","datavalue":{"value":"1564.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025191$16999EB7-6E05-40CD-85E9-B56C901676B1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"888e0a91e6435aac1acb3e29352cb9357611a841","datavalue":{"value":"10.29007/KG4V","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025191$69B6916F-96B9-4581-9AE5-0CBAB2AD6366","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4356e07e26c819aaf28872c09ac7d0a6f42a7b72","datavalue":{"value":{"entity-type":"item","numeric-id":2128806,"id":"Q2128806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$EB94BC88-FE00-4066-B22B-258347805BF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f17059e6c6c8a57972334867cc4d511b5d1368f5","datavalue":{"value":{"entity-type":"item","numeric-id":507357,"id":"Q507357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$5DC821B2-993D-4EF9-9C24-30447F5735FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce9e1735095a7237c0c699c31f4c0eb57566d709","datavalue":{"value":{"entity-type":"item","numeric-id":1401931,"id":"Q1401931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$57FA2640-8144-4057-923D-11AF1361C1BD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d34a2e6c4099712e6f2a5acfda08782bd5ee66f2","datavalue":{"value":{"time":"+2025-02-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7025191$D8662638-4307-400F-876B-EB1028F61835","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025191$95F77230-C094-4030-8284-D5E1BF4B7BFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"176e47af9f9e7cf4ebff07fc1f9e4f94a83134c1","datavalue":{"value":"03C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025191$41FC7B34-B907-4A0F-82E6-26940C8522CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025191$7176D5BF-B033-4745-8FDF-764625531BE6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a7a3b4cb817d98962e7a1e1b747d053352a3f65d","datavalue":{"value":"7986590","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025191$242F354D-BCBB-4CB5-BD34-EF4F5B15AB43","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"be1268b65fc1d6781eb5c0f1073a98e5cb46f217","datavalue":{"value":"arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025191$D8DED2C7-3433-4170-8CD5-B27C072CB643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025191$86D9E7B4-1695-424C-96DD-8809C8BC2BD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8347dcf4505745fc0800ec01edc4707ff42d9285","datavalue":{"value":"LIRA","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025191$3D7C40BC-6C0E-4C86-9299-89F12CB87493","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ce94254d44045733e962d2861c33d94e3725cca","datavalue":{"value":"quantifier elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025191$02F89266-A557-483C-8DB9-1F362C9C07E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025191$73804C97-F954-4C2D-B5E4-4CD51C1CF85F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6a0fdfad23b05e35870737583d90241f6389dd5d","datavalue":{"value":"virtual substitution","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025191$496B9ECD-B6A3-49A4-A4C2-E600D91F7F72","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":"Q7025191$632720C4-2A60-43CC-879F-FA8874AF61DB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3686167e62f64deb45d5189b12825da8941b40bd","datavalue":{"value":{"entity-type":"item","numeric-id":5187396,"id":"Q5187396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$DC786FDF-5D38-481B-B00B-E81E582DF94A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2657b817b7754d2c176503843bf922ca3d3ac15d","datavalue":{"value":{"entity-type":"item","numeric-id":2180222,"id":"Q2180222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$3E9BE017-3FB8-432A-B8D1-43B0D5CA6CAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1645d5977fcbb346c223f2e9f46edf7dc223d58","datavalue":{"value":{"entity-type":"item","numeric-id":4691738,"id":"Q4691738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$9F18DBFB-0853-40B3-8D9B-67789B79A849","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"448e5abb05ec0c10b64746c80e216ef9d23df3a7","datavalue":{"value":{"entity-type":"item","numeric-id":5674430,"id":"Q5674430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$72C8644F-85BD-4BBA-AFEF-0DBEFC931B19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bac46cadd391b69a8eb2eb17270bc333130444c","datavalue":{"value":{"entity-type":"item","numeric-id":6572540,"id":"Q6572540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$7F9FCFE8-1758-4361-BE78-59AB8BA770F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2837eb28569a008677bba2643bbc6df5d206bee8","datavalue":{"value":{"entity-type":"item","numeric-id":4247790,"id":"Q4247790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$4B46ACA6-24C8-4217-8B25-194372E5CEDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37706997c0e12650bf30406d5f3ef502cc6c8e28","datavalue":{"value":{"entity-type":"item","numeric-id":2351157,"id":"Q2351157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$A779E577-98B2-4E5B-B54C-8F63E2CA2231","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ea1a0c9242070effd0bac35bfe23db977c43490","datavalue":{"value":{"entity-type":"item","numeric-id":2879330,"id":"Q2879330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$2D00E60B-485E-4E5C-8E11-AF715FF228D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27230ad583fb6c91e5e0b2ed04e15a2a06ba4a72","datavalue":{"value":{"entity-type":"item","numeric-id":3182526,"id":"Q3182526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$21D6CD32-4EAD-47F3-BD31-3934FE3B8F6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9cfa111152655a1d4c1406d5e37282e85629933f","datavalue":{"value":{"entity-type":"item","numeric-id":5200037,"id":"Q5200037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$1DBBD7DB-FD9F-4ADB-8DC1-558126C8414B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f33ee1e9bddd5e600f5b1d8c8cfae347a7631b92","datavalue":{"value":{"entity-type":"item","numeric-id":3140556,"id":"Q3140556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$1A561F98-4E5B-4633-A5A6-25583F63EDFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d3f5b196c0df4a4076dad9269fa5296f4cdaaab","datavalue":{"value":{"entity-type":"item","numeric-id":1688537,"id":"Q1688537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$66E4F9CE-DEEC-4BE3-9F6F-701ECC2B3341","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64797966d0bed6682a8a82e6f07d143c195878d3","datavalue":{"value":{"entity-type":"item","numeric-id":5120170,"id":"Q5120170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025191$52FF864A-6EE4-4500-8ABC-C9B4BBBB2BB0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"VIRAS: conflict-driven quantifier elimination for integer-real arithmetic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/VIRAS:_conflict-driven_quantifier_elimination_for_integer-real_arithmetic"}}}}}