{"entities":{"Q2554609":{"pageid":2565352,"ns":120,"title":"Item:Q2554609","lastrevid":72775653,"modified":"2026-04-14T07:44:44Z","type":"item","id":"Q2554609","labels":{"en":{"language":"en","value":"Theorem proving with variable-constrained resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3385241"}},"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":"Q2554609$8D8D2583-A19C-407C-9100-6F695FDCCF89","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"27ee7f08bbe2e2d81a833539429f3f21850aaf43","datavalue":{"value":{"text":"Theorem proving with variable-constrained resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2554609$6B048DF0-C502-4E63-B111-F12462CB7783","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2a97013bfbf9269654ee1da7a642106977cd5298","datavalue":{"value":"0243.68011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2554609$607945BB-5F9E-484C-A9CF-7B2F00369A12","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7dbdffb1c2df2528a03667e1c645200373813f94","datavalue":{"value":"10.1016/S0020-0255(72)80012-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2554609$6037BA98-743B-4864-9CE8-BB2A796613BD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc45e6b9322bed7360e4aac2a42f8c73614b44f3","datavalue":{"value":{"entity-type":"item","numeric-id":1787138,"id":"Q1787138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$99C0B796-DEE3-4312-BD42-CFBBEBAB0E59","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c144f0fb88440afe4b13555aedcc8676a016b6d2","datavalue":{"value":{"entity-type":"item","numeric-id":70466,"id":"Q70466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$62CAB7DD-628E-4B5D-A94D-23115985E92F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4bb0eaa1d64c683ee03edf396d2a33ea56290ca3","datavalue":{"value":{"time":"+1972-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2554609$C0DD79B1-833B-4323-AE66-6016318356A3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2554609$05562D7C-03EE-48CA-914C-8616EBC276A2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"54d576469affed82cc6413d4105595259d97944c","datavalue":{"value":"3385241","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2554609$19EC1427-297B-4859-911F-776A281A70A3","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":"Q2554609$6425FD4A-772C-4658-BFD9-BF1ABBAB503D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5ba7db293ebaee9aa1ef89b96577a438c7ecefe","datavalue":{"value":{"entity-type":"item","numeric-id":5624685,"id":"Q5624685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$5555148C-9C8B-4EDF-B10D-054E06B37C6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e19bcc8ceeae09bfe2823325d7d61b377dc18bc4","datavalue":{"value":{"entity-type":"item","numeric-id":5597535,"id":"Q5597535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$848C7DF2-D6D8-4800-A7C5-9C54C43A3606","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89838827382acbf53ce860d7765a55008850713f","datavalue":{"value":{"entity-type":"item","numeric-id":5573405,"id":"Q5573405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$77BDCAC7-C386-498E-8EC3-8C9BC5F05A16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84e0ec301a2daa50bbddaee495d81db74f852f2b","datavalue":{"value":{"entity-type":"item","numeric-id":5613968,"id":"Q5613968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$2818274D-7F28-4115-BAC4-BC4CAC918313","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"963e5e2815a6925f928997ee3899c68354018adb","datavalue":{"value":{"entity-type":"item","numeric-id":2542996,"id":"Q2542996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$6AB5A1A1-EED4-402A-978D-01ADC4DCBCEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33120ae1c57e0f2f7a4bfd99b86bab8f2ace918f","datavalue":{"value":{"entity-type":"item","numeric-id":5649990,"id":"Q5649990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$5A5C67E2-5878-4F5E-A42E-242CA47FCB9C","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":"Q2554609$655DDC95-7C97-47E6-8DC8-898604A63B5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9d6412374cd99d26f25760aacca4ecd0fb813a7","datavalue":{"value":{"entity-type":"item","numeric-id":5339307,"id":"Q5339307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$1425AB9A-A43D-4DCD-BDEA-D3C4D85F8143","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7b078ac6522bcee697c559fd0ddac36e74baef1","datavalue":{"value":{"entity-type":"item","numeric-id":3275827,"id":"Q3275827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$102B09D1-B9C1-4B1B-A634-E7ED149A04A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f09c8478424162622e2e11cbade44966513eb5d","datavalue":{"value":{"entity-type":"item","numeric-id":5621960,"id":"Q5621960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$4A6E3565-F7F0-43C3-8C54-F2FC6A91565A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65f72fa731d5ef46f7c8727b7b59f2eaf22c3523","datavalue":{"value":{"entity-type":"item","numeric-id":5544307,"id":"Q5544307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$07E5DFF7-23B5-43D6-8A82-43A26ABC6EE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08067296a778be982332271922f05534568e2cf4","datavalue":{"value":{"entity-type":"item","numeric-id":5600875,"id":"Q5600875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$BA89FD12-5B03-4F4E-B932-1BBDD18F1102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"123015d988bb6f26763623b31aeabe5ee6b2e143","datavalue":{"value":{"entity-type":"item","numeric-id":5594194,"id":"Q5594194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$52A23B33-37EC-4498-9599-F1BE38575594","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7cc6b50da59d61e4104676cfaa2ed0a6b850865","datavalue":{"value":{"entity-type":"item","numeric-id":5619635,"id":"Q5619635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$E72341D6-340D-47A4-B0AB-395630C06350","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d53a28b01bdaf2102551cb99ed821945979a516","datavalue":{"value":{"entity-type":"item","numeric-id":5541352,"id":"Q5541352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$1B2035C7-6728-4609-A9EE-A549B6D5CBB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1f3e0d3ccdd5ec8618c022752f1b192d7395e28","datavalue":{"value":{"entity-type":"item","numeric-id":5614670,"id":"Q5614670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$53998E76-7453-4A8C-8862-91A74A4CD9A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62e82257b416db4246a715182cdefecc0570e41d","datavalue":{"value":{"entity-type":"item","numeric-id":3279281,"id":"Q3279281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$B4CF95EE-E79A-4990-89D6-BA543D7F61F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cceee8a5fb32e6eb7443356542ae558c36b13a21","datavalue":{"value":{"entity-type":"item","numeric-id":5672214,"id":"Q5672214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$875F786E-D77C-4CBD-86BF-BC68B87E2D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febe5bf101c3b7d6dce19439eb466caa5715de79","datavalue":{"value":{"entity-type":"item","numeric-id":5624683,"id":"Q5624683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$3651DF4D-6CEB-4422-96C8-2D0C0553AB6F","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":"Q2554609$64552930-EAAE-4350-B3D6-F028BAAE96E0","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":"Q2554609$113A6DC8-95FE-4CB9-989F-28A7928341F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1af0fa3ab79d3aca7d0c2eb038f3a2d86af567","datavalue":{"value":{"entity-type":"item","numeric-id":5541351,"id":"Q5541351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$0C832613-8CAD-43E9-B54A-E5E342C9D9CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db57d83c4539b5e1e312a9885e87a573f21cf309","datavalue":{"value":{"entity-type":"item","numeric-id":5562604,"id":"Q5562604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$96C288F7-C465-403F-930B-575C036C46D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e169af1b2927cc066a8cc188c6dd43f7cce9298","datavalue":{"value":{"entity-type":"item","numeric-id":5591533,"id":"Q5591533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$FE1F89A0-AE98-4240-AFC7-8EC968A2C713","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f771f551f48b2f2d21f6f2011008cb21eb26e492","datavalue":{"value":{"entity-type":"item","numeric-id":5538933,"id":"Q5538933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$351D9633-144E-4B39-B246-9E4074491EC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f6b9cd499811e8bf59f5811b67114ca0b6f01e1","datavalue":{"value":{"entity-type":"item","numeric-id":2549243,"id":"Q2549243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$6731AFA8-2DEC-455D-8564-494C0998E226","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11b6f231eb024fbb0248b8ea953dad94e2ed45be","datavalue":{"value":{"entity-type":"item","numeric-id":5507984,"id":"Q5507984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$B8C56547-02BB-45CD-93AD-30D6A4F5D94D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47bab4f7d1b2661e9a9ca3ddc35e5a57311ad582","datavalue":{"value":{"entity-type":"item","numeric-id":5507985,"id":"Q5507985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$BAD95138-8A53-45BA-AD08-A6F2E99EFD44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7053c119e620b9c3b3c8c19da3a6a2d1be1e3c68","datavalue":{"value":{"entity-type":"item","numeric-id":5538934,"id":"Q5538934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2554609$E8FD8995-C8DF-45A5-85D6-66C6EEAF036B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem proving with variable-constrained resolution","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theorem_proving_with_variable-constrained_resolution"}}}}}