{"entities":{"Q4885907":{"pageid":6915486,"ns":120,"title":"Item:Q4885907","lastrevid":46395765,"modified":"2025-12-24T17:05:40Z","type":"item","id":"Q4885907","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 910745"}},"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":"Q4885907$E01F76AB-A884-4FB6-9CF8-B4484E7E3E66","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2bb3c369e379e30cf7f0919cd8b910577209d535","datavalue":{"value":"0859.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4885907$4C9D2661-0FEC-4A08-A490-71ACE4EA0EE4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0af7e025189305bad11f686c710fe3b187470eaf","datavalue":{"value":{"entity-type":"item","numeric-id":438567,"id":"Q438567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4885907$F6F22D27-D95D-4880-99AC-088E4BDCBD9C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"987a2f2e82526aa2085dc97bf2e88574c6b234f8","datavalue":{"value":{"time":"+1997-04-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4885907$D400B0CE-574C-4331-8A34-B0FCD7E1509C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4885907$0AA74262-0ECF-48FB-8B91-CA2506104B54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4885907$C5AFD0EA-DC36-41F2-840B-088634422F2E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6bac7418dd13814cad32240f9e042e7760dd8d22","datavalue":{"value":"910745","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4885907$239E653A-3E0F-4766-813B-F5F37D417EA6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q4885907$0BB9C532-87CD-4D3A-9D2E-574B907A093F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"adcd8cbf799007480045934b55796e5f65596977","datavalue":{"value":"complete resolution refinements","type":"string"},"datatype":"string"},"type":"statement","id":"Q4885907$509E5CEB-98F4-4883-9DF5-B90EAFA67A99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96c60e51dcdc471170f77c46be57db83d1d7ec4b","datavalue":{"value":"resolution game","type":"string"},"datatype":"string"},"type":"statement","id":"Q4885907$42FD0305-3DF5-4533-8062-C7414069490E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"404e591614190488419156400105486d83841bbf","datavalue":{"value":"sequent calculi","type":"string"},"datatype":"string"},"type":"statement","id":"Q4885907$64377512-F02B-4A73-8033-8C2A59196E85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4879e8c35d56fd297a402f7c1eba53238e04d57b","datavalue":{"value":"proof search","type":"string"},"datatype":"string"},"type":"statement","id":"Q4885907$EDAB894A-4CF5-4B24-91AE-0B6C24BBC345","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q4885907$D6975B5E-5DA6-48E5-9075-C4BE5DABD2D8","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":"Q4885907$EB6DA539-264B-4B27-BA6B-12AEBCC3F32B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f8b31950da2321995a2d95a15e67ae6d16ba9e9a","datavalue":{"value":{"entity-type":"item","numeric-id":4474846,"id":"Q4474846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25b9d8c55048683b95213dea3c4894318a6de23d","datavalue":{"value":{"amount":"+0.8632022142410278","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":"Q4885907$9A885D4F-A4D4-4656-A115-E361EC150D05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48a3d434253ed919faa661b14e883ac27b635cfa","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"378183dff7598204a130b7c8d6545258b44aa471","datavalue":{"value":{"amount":"+0.8031973838806152","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":"Q4885907$1329AA0E-91C8-43AD-921B-4F94FE6B7AD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c0c6762ed4becc0db8d77028d41650996045021","datavalue":{"value":{"entity-type":"item","numeric-id":5713749,"id":"Q5713749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa5a70794a2c5464dd5349e0be8fedc79d835877","datavalue":{"value":{"amount":"+0.7720615863800049","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":"Q4885907$2E26C361-D700-4A0E-B9EF-D4BB746682F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d774b848aec03fbaa972ca7064d768c2b50c6b3","datavalue":{"value":{"entity-type":"item","numeric-id":2751377,"id":"Q2751377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5091f8847a9c6597e895f3c87cecec1260cc899a","datavalue":{"value":{"amount":"+0.7640393972396851","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":"Q4885907$2515919C-19E3-42BE-94DE-A6940FCD19BF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4885907","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4885907"}}}}}