{"entities":{"Q2864408":{"pageid":2875128,"ns":120,"title":"Item:Q2864408","lastrevid":79490537,"modified":"2026-05-06T14:01:56Z","type":"item","id":"Q2864408","labels":{"en":{"language":"en","value":"Encoding first order proofs in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6236412"}},"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":"Q2864408$262B1A16-61BA-49D0-9895-D28E3D1BE13E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"58bd3f6b0693b957700e396f86761f035fdd6c9a","datavalue":{"value":"1277.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864408$D57F930C-3E0E-4D6B-983B-74E7A8428067","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"33e4d7bdc073a84821ca343c7b634dfa88029616","datavalue":{"value":{"entity-type":"item","numeric-id":2864405,"id":"Q2864405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$61DCD532-2FF8-4984-B8AF-CAFD3B53B0C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7fd61eeb173b8512626573d7cfc4d27f601565f6","datavalue":{"value":{"entity-type":"item","numeric-id":2864406,"id":"Q2864406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$ACCC091F-7A62-4981-A16A-F43811648FB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"19f22880441832c1cbe5bccc835bfadba3b4fd22","datavalue":{"value":{"entity-type":"item","numeric-id":437035,"id":"Q437035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$7C5E8147-4C2B-4457-8637-2E5928482C6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b74f2805d58a252b355491b4dc993b2648b5d8c","datavalue":{"value":{"entity-type":"item","numeric-id":437036,"id":"Q437036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$F56D9954-18CE-4BEF-A163-EF71BC44574A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e5b1a29cb7ce49c1bc5bf2d17c64792b9ca38181","datavalue":{"value":{"entity-type":"item","numeric-id":2864407,"id":"Q2864407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$469E92C0-8055-4A73-8B93-EBC30E0A8D4A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$4F72F310-8A23-4AC3-A2E4-DD04A7104787","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"deb6cb3450bd256fc635dc32234471403070c2b7","datavalue":{"value":{"time":"+2013-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":"Q2864408$2C00569D-DB7B-4022-9D41-7FF1FB406F6E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864408$1008390A-73DC-435F-A0BB-620C640F7D98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864408$C94A94C6-257C-481A-88F9-1CF61F85E358","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ebdd1b7928d71d996a2808cb2d9d873a997be26c","datavalue":{"value":"6236412","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864408$D2BEB9CC-6ECD-4B17-A627-E11E3925E456","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864408$3148DFA4-AB0A-4187-9AAF-2C9E419822FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864408$B46C56DF-887C-41F5-9697-3B1C9A893A6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd47118910fdb38c46f5f4fe99e3757adf12edc8","datavalue":{"value":"tableau","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864408$612CA03D-028B-4A48-8A57-EA13FDD5FD63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd8ba7e58aca96f1c796c3939a1dae132ee43860","datavalue":{"value":"Yices","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864408$B0357AB3-07F9-437C-9572-171B26BEC03D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"da57235fa8e09bd38824101830612d766e9fc5c4","datavalue":{"value":"Q118190444","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864408$9B28FACF-401E-42C3-801A-BA5F8E215BF7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$28E85805-1793-4B99-8BB5-7BA75993DDE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$E6C899DF-E45C-4F82-9647-1BDA6BA92AAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$3C267305-8AB7-4BC5-AA9C-F6962FEEA9E1","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":"Q2864408$4AB603B6-B007-4A93-B550-D8E03B97DB34","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9a349048d13eab68df584f1b1123b87850df4987","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2008.04.081","type":"string"},"datatype":"url"},"type":"statement","id":"Q2864408$CA6D7C17-2360-45CC-B4BF-0B29601B2B76","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b31681619662524252d68e56d5d8c8a0a7b72bc2","datavalue":{"value":"W1975097530","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864408$ACCA6F32-098E-42E4-8233-F5C1B70E1FFF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ed4e2b73edd0e2661ebb75822eda29ecb9eb63a","datavalue":{"value":{"entity-type":"item","numeric-id":3906484,"id":"Q3906484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$E37F9DC6-E412-41D8-BC96-D90F1129E9BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4da258b65e2346205134973cc333997cb45b7692","datavalue":{"value":{"entity-type":"item","numeric-id":5570212,"id":"Q5570212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$6CA8E0C1-140A-4051-BCEF-E86747DDA64B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$12B442DA-5BDF-4B8B-81E7-17D60EB4086A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$4AEF82A4-FA77-45A3-82FE-F73754623BB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"127fc404d70d2c74792e0fa1dce28f9cd95c3e7d","datavalue":{"value":{"entity-type":"item","numeric-id":3498469,"id":"Q3498469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$1E82C317-A55D-4801-96AF-D6C810557BC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b547ecbdee111d500340a1755c27397d76f7d718","datavalue":{"value":{"entity-type":"item","numeric-id":3608794,"id":"Q3608794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$2634B317-3D86-46BC-8021-3BAA06E75802","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"32e3d836818c9b82aae57d28f4250382c391217c","datavalue":{"value":{"entity-type":"item","numeric-id":4942635,"id":"Q4942635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$B5B8C0CD-CD1F-464F-89F4-8A180638B99A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17e9e44d7ffa3e35b73497e32253991279784e6a","datavalue":{"value":{"entity-type":"item","numeric-id":2751354,"id":"Q2751354"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$ED71EEC0-6D32-4485-8FD2-4A06F0228AAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd41301b78a03236dc27ccdfce83b246065d0cdc","datavalue":{"value":{"entity-type":"item","numeric-id":2751380,"id":"Q2751380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$1EF2AA1F-3728-462C-998A-5C096BD2A428","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$F122E1EA-D734-4CC5-BE88-FDEF5D7AE907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864408$4FD63D5F-95F2-4DDB-B929-B76BA4E7E068","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3dbb31a550759f305a2a9f4800a63d53fc79a886","datavalue":{"value":"10.1016/J.ENTCS.2008.04.081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864408$8E71B8B4-6D31-4142-85A6-6A0A85BF9788","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9739f25591577d2cbec5f1bc44d5adf461fe1995","datavalue":{"value":{"text":"Encoding first order proofs in SMT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2864408$ACBF7FB9-B48D-4E11-BF70-614A011EE602","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5df8826be1b5b58b3b9a0717748031d96b7a3c19","datavalue":{"value":{"entity-type":"item","numeric-id":3608794,"id":"Q3608794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64b8ed338e069c8a76db229ec35bf1c7095aec3d","datavalue":{"value":{"amount":"+0.8843302726745605","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":"Q2864408$E94152AE-5AD6-4165-92B0-C141E7E3DAAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d5968f2b23fcdc9731d7a84030bc488254fda57","datavalue":{"value":{"entity-type":"item","numeric-id":1799100,"id":"Q1799100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b0e9c6a49e3024f12b16e4131b2b65be4a7946d","datavalue":{"value":{"amount":"+0.7162806391716003","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":"Q2864408$C12ED791-D65F-49FC-A581-0FE0C93A585B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"353b46cb2a124cc2200384a940b087517c5b273c","datavalue":{"value":{"entity-type":"item","numeric-id":1037239,"id":"Q1037239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92d687bf87b1f0450bc6b07d5febfd30c64f1df2","datavalue":{"value":{"amount":"+0.7103695273399353","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":"Q2864408$24B40EB6-E45A-4E79-81C7-6F70F0E3A434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c346a30c2b2aed7868880120d4d7c225af677033","datavalue":{"value":{"entity-type":"item","numeric-id":6039408,"id":"Q6039408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77a6fd1367cc9faa9b62c7bdd2c1cfbc6a5d7267","datavalue":{"value":{"amount":"+0.6922158598899841","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":"Q2864408$283A0149-3726-4966-AC25-CF9A31B27430","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"062a7b7580365074b64d54fe631d8b6c277e8274","datavalue":{"value":{"entity-type":"item","numeric-id":2974796,"id":"Q2974796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93de2663b883fae9f8ea6a1829de45f44054cc9e","datavalue":{"value":{"amount":"+0.687520444393158","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":"Q2864408$CC9747BB-4BCC-450D-9EF1-D88F33782106","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Encoding first order proofs in SMT","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Encoding_first_order_proofs_in_SMT"}}}}}