{"entities":{"Q5443571":{"pageid":7473129,"ns":120,"title":"Item:Q5443571","lastrevid":96333839,"modified":"2026-06-05T10:58:32Z","type":"item","id":"Q5443571","labels":{"en":{"language":"en","value":"Another look at automated theorem-proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5237805"}},"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":"Q5443571$C33CE24B-A3F6-45F1-A275-0253AD39D6DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b65d169535f083ea4ec65add0f3ecdb636527425","datavalue":{"value":{"text":"Another look at automated theorem-proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5443571$4645656B-E3FC-4B54-8EAB-E09303F47F6D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"27a5a7cef66f384a758f44167a10fb0431985c26","datavalue":{"value":"1132.68681","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5443571$A2E4D05D-5ECC-4016-982C-59E47E01C59A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b1bd9c533d29c9e868404d44a634953355789945","datavalue":{"value":{"entity-type":"item","numeric-id":384279,"id":"Q384279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$942E0033-97D5-45AA-8E53-7A662F630418","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52d43017492cad5b25a46de83afd30a61ffd99d6","datavalue":{"value":{"entity-type":"item","numeric-id":269100,"id":"Q269100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$7B8327A9-60CE-49A6-88B8-FA4423C5104E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d8a77078870e75a3ff7471ca3f5350a598b0be6d","datavalue":{"value":{"time":"+2008-02-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5443571$18CCF24A-9EEB-4203-9BE9-0EBC5D025BEF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5443571$AD3E7DBA-0E92-4BD3-BF15-66325F9977A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b3f5570531d36cdad95fcc8cba24a2dabc5fbbbf","datavalue":{"value":"94A60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5443571$7843B8F4-0816-478C-88FD-41BBC841B4E9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"615354318e329a75a0fa12f4ddf8a057e083d05e","datavalue":{"value":"5237805","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5443571$D104E389-57F1-49CF-BBAE-0AF00B2EF7E2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc0a06ffadbc917396a626e33a9a5489bfbfb917","datavalue":{"value":"automated theorem-proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5443571$8CD878E5-ED86-485E-BE39-9A40B71517AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"88524e08f921927037ac8f544920df56683b67bc","datavalue":{"value":"proof-checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5443571$D4C225AA-280C-40CE-891A-4520AC272F9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b5ca4758585207487a4d04aaaf2698eac445330","datavalue":{"value":"public key cryptography","type":"string"},"datatype":"string"},"type":"statement","id":"Q5443571$32C1BEB7-4453-43F6-9763-075B69F43AF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d873a1d4d05cb79d90b13271e3f58ea19f26e91","datavalue":{"value":"signatures","type":"string"},"datatype":"string"},"type":"statement","id":"Q5443571$32B7CE66-AA11-4D7E-A13A-9A4BD04D5E85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02b80c2847a486b7b7a3e208de90f06ffb8afe61","datavalue":{"value":"encryption","type":"string"},"datatype":"string"},"type":"statement","id":"Q5443571$5AA75D6A-CD5A-4E13-9A08-C8E582F78928","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":"Q5443571$9D55DB7C-4B2E-4CF2-A9B5-99ED2FEBBA3B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c8cc4c8581eee0044825b1cdafb82959f21b3b7d","datavalue":{"value":"https://doi.org/10.1515/jmc.2007.020","type":"string"},"datatype":"url"},"type":"statement","id":"Q5443571$69157E7C-22B5-48DB-AE71-CE8C4D4D283D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cbfddcc5254828ad6f50b34933c83ddf58353cc0","datavalue":{"value":"W2040200723","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5443571$76B729A6-8B7B-4EC0-9A19-DC79CF045502","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"aa269326b3937d16eea2777bf8ac10eca53c98bd","datavalue":{"value":"Q58043219","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5443571$2548EEE2-6130-48F9-9638-D108B0CC0477","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"deff1d3d5e1b103ae88f86df1e2ee615c0f90bd1","datavalue":{"value":{"entity-type":"item","numeric-id":5756645,"id":"Q5756645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$D7582193-F774-49B3-BE01-3C9E88B02722","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d56256abc802efd9a03def45c3851c2ed9b57035","datavalue":{"value":{"entity-type":"item","numeric-id":4441904,"id":"Q4441904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$43480EA4-9F47-4199-9F20-1BE741FD17FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4a73265bad6ea50fe9fad5bfba6b38941e6752f","datavalue":{"value":{"entity-type":"item","numeric-id":3968876,"id":"Q3968876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$2EDC9A46-9368-426C-AFA0-63101819106E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b548fb76f8ef8a56f9223030f407f1a96f0c7ba1","datavalue":{"value":{"entity-type":"item","numeric-id":1057832,"id":"Q1057832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$B132AD6D-29EF-4911-B28C-A120069D262D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b559443e13096aa253418e5dea9b3753c3e0250","datavalue":{"value":{"entity-type":"item","numeric-id":882771,"id":"Q882771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$80742FA6-0303-450D-9208-F4318AE574B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e971d54c4969e46a7ee5ae5ebf843d1f684ec82","datavalue":{"value":{"entity-type":"item","numeric-id":5451048,"id":"Q5451048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$312E3A97-40C7-433D-AE3A-93A859CBB875","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88340151a17dace366bf5d0e0e03ca13bd516ba8","datavalue":{"value":{"entity-type":"item","numeric-id":5443562,"id":"Q5443562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$0BA5D3C3-BA4E-48D3-AB89-CE6BE6690F6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d706128b6832cad5d41d6b4b51dd069d3fb2e7bc","datavalue":{"value":{"entity-type":"item","numeric-id":5458271,"id":"Q5458271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5443571$0F42B3A3-5409-41F6-A6D2-F1BB85735A2A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"031faa2b001823d1cb9c3634dfc432fa5c93bb86","datavalue":{"value":"10.1515/JMC.2007.020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5443571$663A2E31-65DE-4F7C-8828-57538C7D8C16","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8501b6b04cc55db58b8949e992a91b67e2c314d1","datavalue":{"value":{"entity-type":"item","numeric-id":3225748,"id":"Q3225748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5b798252250bdae67ea2885ed022b5a795ace34","datavalue":{"value":{"amount":"+0.9107882380485536","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":"Q5443571$0D52DCE7-2557-4F36-9C47-FE48E572CE53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3fd574059b1fbf5aa99d2abc68db3d7d3fd4817","datavalue":{"value":{"entity-type":"item","numeric-id":5756645,"id":"Q5756645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb964cede1df8cd80413566a2929eaaaa537250b","datavalue":{"value":{"amount":"+0.8283767104148865","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":"Q5443571$76599BF3-8420-4553-A6A9-23304B006E00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1aa4625440697f2ee72d406a46d1e48df0580662","datavalue":{"value":{"entity-type":"item","numeric-id":2914729,"id":"Q2914729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd1bdcd43a29b801cde3bce58789d88e5e92c959","datavalue":{"value":{"amount":"+0.8127555251121521","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":"Q5443571$02374154-D5F9-4432-BDDE-C6EDF2E3A0BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9970926fb663e97cfa6d9724fe0af1a4b64d0fda","datavalue":{"value":{"entity-type":"item","numeric-id":3044257,"id":"Q3044257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7922649b32434749f6a17ef54e6ccf2501d1663b","datavalue":{"value":{"amount":"+0.8008489012718201","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":"Q5443571$2BF6E4CB-AB26-4A15-9B35-16F915081183","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25d9e71426cf434c375ccc2ccd842157c240e198","datavalue":{"value":{"entity-type":"item","numeric-id":5199185,"id":"Q5199185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ef10213c1b72acc33c82e72e5ad6d59d860cf1c","datavalue":{"value":{"amount":"+0.7974671125411987","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":"Q5443571$94F7FA0B-AC97-4319-B005-F70D263A06F3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Another look at automated theorem-proving","badges":[]}}}}}