{"entities":{"Q1337680":{"pageid":1348419,"ns":120,"title":"Item:Q1337680","lastrevid":67616571,"modified":"2026-04-12T19:02:56Z","type":"item","id":"Q1337680","labels":{"en":{"language":"en","value":"Problem solving by searching for models with a theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 683693"}},"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":"Q1337680$1EAD1ED3-CFBE-4AA6-A0DB-1EDB044B4ED2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f195a4b50c08b159f4e14f5eee49cfbcc2b146fd","datavalue":{"value":{"text":"Problem solving by searching for models with a theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1337680$E280DFF5-70E8-43F2-A44E-DB2B72F37669","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"676b181bdbe212c5a6ba4e6dbe5e8381c37c5814","datavalue":{"value":"0941.68740","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337680$3657E575-8EED-42DC-91C6-05F7E69BDD62","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c4ddb76d18cc90d238e06014996dba470faea4de","datavalue":{"value":"10.1016/0004-3702(94)90082-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337680$7B134F8B-3AF6-484D-AD0A-6F8FABBB492E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f5f8c560f95a3a7e60d41630a8b70745f361623","datavalue":{"value":{"entity-type":"item","numeric-id":528695,"id":"Q528695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$DBA54CA9-1793-47D4-BF2C-58A8F5E64C05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"34f99c9947f4d98af9da609b6496b55645bbe075","datavalue":{"value":{"entity-type":"item","numeric-id":1238600,"id":"Q1238600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$A124B4B2-D8C0-4BF9-A8B5-A9E6DC2C420C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"984e6510ec40a363d20e607cce2cc2f8b07918ae","datavalue":{"value":{"entity-type":"item","numeric-id":72340,"id":"Q72340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$6F1473D4-9B71-479B-A793-B62316017CAF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7ea9b73e56331fa959af81c0395e4a2ba116b3ca","datavalue":{"value":{"time":"+1996-02-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1337680$8DB163C5-23A5-40DA-B7D4-01D8963808B7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337680$B54721CB-0A1E-41E3-AE86-0F8DCA3601EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337680$A0C1CC38-362E-4551-A542-A10838827114","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e95600064bf1b8c3f256e7bd99dd8ce738f08b8e","datavalue":{"value":"683693","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337680$EB19DB78-2DBE-43FD-AE9D-98363D478BA3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$3A1F14DB-F163-4360-8165-C2AA96266A08","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":"Q1337680$CDF319EA-798E-4E34-A316-2692C64026CD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"75299ac24bda769232fa631f37023f05347dd5af","datavalue":{"value":"https://doi.org/10.1016/0004-3702(94)90082-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q1337680$1F8F7675-EC5F-4D39-96FC-FF124EEF0F68","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5c90846e578305165731603282ad9fd9757fefad","datavalue":{"value":"W2047274827","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337680$88642538-EC4E-41BD-9A9A-BE44FAFCA5FC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2c2b382c3725436e250ac6e5f951d42a292c14","datavalue":{"value":{"entity-type":"item","numeric-id":3954845,"id":"Q3954845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$190ED6DB-6182-4447-B457-42C58864D7DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$F7AFB62B-5629-40D0-8C42-57D1F3FBA113","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18e02e9c674d233134ea38fb41ce14c527d11d38","datavalue":{"value":{"entity-type":"item","numeric-id":4431379,"id":"Q4431379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$7AD50D97-6EB0-4C55-82BA-2CD6B5811612","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":"Q1337680$018CE2F5-CB17-4E7C-94E5-466475F3AEB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b7948d2ae997be513a92df2486b836c4e1eaa12","datavalue":{"value":{"entity-type":"item","numeric-id":5667480,"id":"Q5667480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$3E5015C4-253B-4019-8BD8-D2111B6B536B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$BCE56E56-0451-4219-AC69-0C40C1A4386F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a170af516145ca9c0e5963c08cb024ad4f2af17","datavalue":{"value":{"entity-type":"item","numeric-id":3489523,"id":"Q3489523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$86F718AC-9930-42A7-9D6A-63CAA0C31EB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afc61a2037feef2b958c658698dd68bdb6481612","datavalue":{"value":{"entity-type":"item","numeric-id":1102137,"id":"Q1102137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$562A55C0-E15A-45C7-A2C1-B58BB1DEF6D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3322157bf6a01189b1807437698fe608048635ac","datavalue":{"value":{"entity-type":"item","numeric-id":4167597,"id":"Q4167597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$6CC6501F-FB94-4370-88CF-43C38047718E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a35cc55e5b10a424a85f3ddcd5c540cf5328ff0d","datavalue":{"value":{"entity-type":"item","numeric-id":1249435,"id":"Q1249435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$89C6EDC1-8FCE-4392-9B9B-98FE5E3B71CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be5611a6f60e59f1388392174f8631ce9b0f98d8","datavalue":{"value":{"entity-type":"item","numeric-id":3789107,"id":"Q3789107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$B566A2C4-810D-4C21-B71A-F902B25ECBDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fba5a1fdfac74b8e0dcefe0e56f5b10792486d","datavalue":{"value":{"entity-type":"item","numeric-id":688547,"id":"Q688547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$98A26C3B-76FA-4423-8AA8-5D25208BF92C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d6e5a2ec66a572177ef7c34d7ff9e3c5a3050d5","datavalue":{"value":{"entity-type":"item","numeric-id":1157324,"id":"Q1157324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$CF89A1C8-FD0E-454E-8C21-DE5EA9E339FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$EF68D992-8FE8-4BE2-BA91-552A49F3B675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26e765697dc730e487db4a5421dc5ddcece8b423","datavalue":{"value":{"entity-type":"item","numeric-id":1819949,"id":"Q1819949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$CDBA1569-A4C6-4B25-A0F6-31BEB81DBE78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1bc7b0f82e42c56ee306811b6c3df8af19432e03","datavalue":{"value":{"entity-type":"item","numeric-id":1231783,"id":"Q1231783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$B1D3D2FA-85ED-41AF-85F1-9F8ABF340F8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0081b258510dd8e01215933d88134a958186d290","datavalue":{"value":{"entity-type":"item","numeric-id":1075318,"id":"Q1075318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$13D73D12-100A-4531-A0E7-C37DB1EBD496","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43919d1f4da3b9a07eea3d230b3f18d880d5940","datavalue":{"value":{"entity-type":"item","numeric-id":1116717,"id":"Q1116717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$8B977266-D3E3-4886-A0D2-E97C88040BF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b731cd316d5d0e7983ec5525ca4b9f954aaf858c","datavalue":{"value":{"entity-type":"item","numeric-id":3484382,"id":"Q3484382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$67D7CC65-2CDE-4C36-8376-9D4D9D37E22B","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":"Q1337680$2BE55E02-F8CE-4D59-90F1-00AE2A6928C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adbfa02ab4b7e0bb252f5a5604936a94deac79e9","datavalue":{"value":{"entity-type":"item","numeric-id":3847756,"id":"Q3847756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$B1E780B1-69CF-46A3-9FEF-7C2A9A24AD30","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":"Q1337680$907362CF-31DE-4C6F-A201-66D45302F8C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03b5ec7b36ab9f9a9396a2be7f7246c57825af23","datavalue":{"value":{"entity-type":"item","numeric-id":3742689,"id":"Q3742689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$6FAD67E0-4721-4117-B0B1-15B77F1AA195","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab938ba3d2bb1de7d34dc0f9166735f59a48b21","datavalue":{"value":{"entity-type":"item","numeric-id":1114446,"id":"Q1114446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$9DFD2A24-5987-41E7-9073-CE1D9371E5D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ef75b4b5ae4f1119c1ac9bfdcf91039dbf37c93","datavalue":{"value":{"entity-type":"item","numeric-id":3829089,"id":"Q3829089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337680$8507EAC2-88BF-4DDE-9BA2-5A2F2E883749","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Problem solving by searching for models with a theorem prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Problem_solving_by_searching_for_models_with_a_theorem_prover"}}}}}