{"entities":{"Q831945":{"pageid":833793,"ns":120,"title":"Item:Q831945","lastrevid":64783896,"modified":"2026-04-11T22:12:03Z","type":"item","id":"Q831945","labels":{"en":{"language":"en","value":"Quantifier simplification by unification in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7497925"}},"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":"Q831945$1EA9EA4E-51F7-4EE1-821B-4112E8C23267","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6d88aac30e2bdbb997a8123345e0c1d2e546726d","datavalue":{"value":{"text":"Quantifier simplification by unification in SMT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q831945$7C197EDA-A220-40A5-A4A3-2890FB8C4B74","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9fd2dd45d8cd14d8f9ebe26c5c81b36722fcea45","datavalue":{"value":"10.1007/978-3-030-86205-3_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831945$26489D09-172B-4F6D-8B4C-96A3AA650144","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"17d182828bb3dd01cff9766a0bb3efe1eeb4424b","datavalue":{"value":{"entity-type":"item","numeric-id":436375,"id":"Q436375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$AACC0651-F393-41A8-A07A-D8BC1D0DE687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"43d7ec59f5db7e89994eb5f4a130aedf59ef13bf","datavalue":{"value":{"entity-type":"item","numeric-id":831944,"id":"Q831944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$E092C867-C85E-4D8C-9C84-C976C92788F2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ee216241628d7ab3ed1211164658dc9e68b98545","datavalue":{"value":{"time":"+2022-03-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q831945$1991A500-570C-4C7F-A350-EEE83622D7A8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7e15970bc23e4f7ac1ca5021e8c1c3e94a2464e0","datavalue":{"value":"https://orbi.uliege.be/handle/2268/265881","type":"string"},"datatype":"url"},"type":"statement","id":"Q831945$F8CA1AE9-B6B1-430A-BCD6-7BF2238D008C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"18309be7db1da1fcc09fdceba48f604c7de62db3","datavalue":{"value":"68Txx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831945$4F6CFF55-F076-4965-80C3-42445815A90A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78250ce3d6d1cf6b13a3fc52b202eccd8ac340b8","datavalue":{"value":"7497925","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831945$069AAD1B-0B13-440D-8959-0BF2B9AD03CD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q831945$9859DA35-F493-4718-A6B3-74F7CD80C30A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0764fa593d7e4a1ba11a6e2681d8d16e893c29d9","datavalue":{"value":"quantifier instantiation","type":"string"},"datatype":"string"},"type":"statement","id":"Q831945$29082830-2914-40A3-B0B2-AF377A28404D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q831945$6CDEFB1A-1138-4855-8712-3CFF955A5F81","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90c7c18880caa813a6bdace0f373d3dec3147690","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$C3366353-C111-4329-AFC4-2AB913261F7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$3B095817-987C-4EE6-B062-19FD737F78AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$D3CB3EFE-2DAA-4243-B7FE-593A23E76D81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$921EBD62-F074-43D1-97E4-79AC469646B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$8AD0D1A0-E634-4DFE-B0F4-8757954857FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5df14ee9c6f65085bdee53a419634b2235aa5c43","datavalue":{"value":{"entity-type":"item","numeric-id":19326,"id":"Q19326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$F341EEDD-DC58-4AFB-8F54-B05E7B399F4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5b9460a01ea60cde385cddccbe3b63d66f761f84","datavalue":{"value":{"entity-type":"item","numeric-id":44021,"id":"Q44021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$A1997048-27D6-4E5E-8798-E6D5C9AF2BD9","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":"Q831945$BA3DFC3A-A730-4009-B235-31D1C148A903","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"dfe0f8e0aab088ab87d52d47dc8db239ba9181af","datavalue":{"value":"W3197046268","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831945$EFB813ED-B91E-41D3-B23B-298512255539","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9d43b2a1f5b23f5e07e09c2947ef1c6f323b764","datavalue":{"value":{"entity-type":"item","numeric-id":2751356,"id":"Q2751356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$2B02B6D3-420A-48C8-B4C1-8272C33AC0F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db081a6ba37b413fd57cdd13b256d1f5696aed3d","datavalue":{"value":{"entity-type":"item","numeric-id":3303931,"id":"Q3303931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$4D3C2966-095A-42ED-88A9-C8544577B911","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a5f7ec14119349332290c2a3236ae73e2231fc2","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$6527B861-7C80-40D8-BE50-D6937A9A75BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f85fd02f887f9e6cdc6efa73686f469882f2acf7","datavalue":{"value":{"entity-type":"item","numeric-id":438533,"id":"Q438533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$E7B2560A-51BA-407F-82E6-D2470EF2D35A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$C4BDCC15-E918-4C9C-AF5C-47E4316FE67A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b61ff436ad097e7899027abdd6e0c42fca0ee2","datavalue":{"value":{"entity-type":"item","numeric-id":2164216,"id":"Q2164216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$1BA4CABF-EBA9-4982-9D4F-616EABB40E59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d425524c539f34b2c20b8cfec23a758c1eb81a6","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$6207C080-9FF5-4C3D-ADF2-656ECBC31CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f426d61b5e73f09c762af22502a76e1d6d446b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$D315BFFE-C5F7-4B06-BFFC-9F97DE21EF35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$60D51B0B-D366-4839-881F-C14D52C66EA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a8f27245772c2159d3ccf93c502a4163695153f","datavalue":{"value":{"entity-type":"item","numeric-id":3541724,"id":"Q3541724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$5F460725-D5B6-48BA-A9D8-404B88D9A7F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"516924fffc5ccd06ddf357b776bed9baac4d2e69","datavalue":{"value":{"entity-type":"item","numeric-id":2324227,"id":"Q2324227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$FEA5E4A0-DBAF-4084-B218-C3958E0E038D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$E8DD7445-D086-41E4-A0E5-BB7C4A82418F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61d2acfca0f5dfd32b373cf14812fef011284ac9","datavalue":{"value":{"entity-type":"item","numeric-id":2055877,"id":"Q2055877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$FD483EEF-751F-4F0F-8070-31B8B2439827","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f707d41b44671464c5d9fbd310386196c74d6c07","datavalue":{"value":{"entity-type":"item","numeric-id":2751378,"id":"Q2751378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$C1B779BC-6C25-4BB2-96DE-5797AD5BC9EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831945$942699E6-7DA2-4997-A007-B837666EFF15","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Quantifier simplification by unification in SMT","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Quantifier_simplification_by_unification_in_SMT"}}}}}