{"entities":{"Q1404980":{"pageid":1415720,"ns":120,"title":"Item:Q1404980","lastrevid":67521933,"modified":"2026-04-12T18:34:28Z","type":"item","id":"Q1404980","labels":{"en":{"language":"en","value":"Depth-first proof search without backtracking for free-variable clausal tableaux"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1970573"}},"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":"Q1404980$5F0B1F4C-78AD-4B51-AD0D-1CD2CB0D060F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"06a8abb956572bee6bc9da17b0329757c7917697","datavalue":{"value":{"text":"Depth-first proof search without backtracking for free-variable clausal tableaux","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1404980$41B779AB-AB72-4B07-B77A-3CAF5669843C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2d17d38f4b45df25a272e415de2a07ef2eb4cb85","datavalue":{"value":"1019.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404980$78AFFB09-B94C-4BF2-A093-EADDB6A396B5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"758ca3fdf7c21ff4f43a210651a3acf672fda2fa","datavalue":{"value":"10.1016/S0747-7171(03)00026-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404980$DB558B19-CE78-4C2D-B79E-017B6EAF40A3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"573cc3758191477e0c4b208110ac7ed93fa98f2b","datavalue":{"value":{"entity-type":"item","numeric-id":229746,"id":"Q229746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$C83FD00F-F040-48FE-898F-EA9004A25333","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$853FFDD1-D30A-40C3-B710-680322586928","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"988a1f1f38c2f749de54c12ebc5774f827c2b17e","datavalue":{"value":{"time":"+2003-08-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1404980$B4065089-0A0D-446D-8955-B170BD05B7AD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404980$A2922C6A-5A9C-45DB-BCDC-EBB503AFDB24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404980$16FF48B3-3FE5-4CC4-800F-645515DDE276","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"21c20a5166786c3193065d9fdff57cc8fbca2348","datavalue":{"value":"1970573","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404980$846F0B71-E578-4190-ADFF-84D995B90277","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e7920719e7da5d70834fd10ac918c63542f8884","datavalue":{"value":"deterministic proof procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404980$20D400B7-4ECE-4B93-B9F8-C2F99B1CC8CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"189ddca348fe133f20bf892b710bb84987c6e9a0","datavalue":{"value":"free-variable clausal tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404980$364F29C2-15A7-4144-BC3C-895147A3A9F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22732c5512b2ae92675e2848086418a39914f0dd","datavalue":{"value":"depth-first proof search","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404980$81EC6FDE-7657-4816-B674-70E8D95092CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9f277827389dc7b7b895628f120b604cf8435816","datavalue":{"value":"fairness strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404980$78929951-BD80-42C0-A63E-A37CC03A8E55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"628ad435f142d8d8c80673526425fc3fcae5482a","datavalue":{"value":"free-variable calculi","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404980$58CF56D1-E70B-4DF1-8DF5-C930070D607D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$936F7531-FB9A-4DA5-8506-8950346E5B7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e789552fbc9aecbb651052e981d7602fa3ea5d35","datavalue":{"value":{"entity-type":"item","numeric-id":38054,"id":"Q38054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$0E0B1278-17ED-4649-9DF4-1566856E20E4","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":"Q1404980$01EC26B9-3337-475D-9170-2039D9B53FE0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e3a15edbbace0d07f7ac24c32c80a198d5e25a0","datavalue":{"value":{"entity-type":"item","numeric-id":4263168,"id":"Q4263168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$F41DBD01-D57D-4799-9DFF-46F04A052416","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f9349656fac414ddbc9c05d7577bc59cbdac9a2","datavalue":{"value":{"entity-type":"item","numeric-id":4524782,"id":"Q4524782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$D526B790-3FD6-47D9-9DE8-2CDCE9759D4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2aad2916b073577856c022bdffa0d3b878301ba","datavalue":{"value":{"entity-type":"item","numeric-id":4645231,"id":"Q4645231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$DD0EFDA0-9F53-4EB1-A54D-86DE61A8E2C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ad2e3e71fd34316c4d5dca241131f17edc1acca","datavalue":{"value":{"entity-type":"item","numeric-id":4863622,"id":"Q4863622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$BEF8F6C8-BCB0-461E-96B3-F681C9417502","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f33c7e2fc71303fd900c50bc37fd6728d3f12f3","datavalue":{"value":{"entity-type":"item","numeric-id":4539640,"id":"Q4539640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$34651CE0-0C8C-499F-B579-84E5F5F7CF6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1744d65dba6fee802210104b900d9a1f65ede7","datavalue":{"value":{"entity-type":"item","numeric-id":4610325,"id":"Q4610325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404980$48892E0C-B7D6-43B1-8BC7-F224383F2C61","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4b831efe4762ed863b6b406fbe78b5f5efccbf5","datavalue":{"value":{"entity-type":"item","numeric-id":4524782,"id":"Q4524782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78f9278a5184cd38aaff592950983be2005591df","datavalue":{"value":{"amount":"+0.7869724631309509","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":"Q1404980$9441E020-87DD-4E9C-8153-5908BAD18B5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d60c745e4299f3e115acc0b61cab483358f34bae","datavalue":{"value":{"entity-type":"item","numeric-id":3809765,"id":"Q3809765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78f9278a5184cd38aaff592950983be2005591df","datavalue":{"value":{"amount":"+0.7869724631309509","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":"Q1404980$04F73EF1-9FF7-4A0E-B8DC-84527C074C61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f67cf830e08fb9dd462bb8a64126e0aefb31f39b","datavalue":{"value":{"entity-type":"item","numeric-id":5434490,"id":"Q5434490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d27e1ce68ec4d408aec3fd1cc43b337637d9980d","datavalue":{"value":{"amount":"+0.7819768190383911","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":"Q1404980$35625E7B-C8F2-48FF-B4AC-B256BE779CAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8bc8c4d5ed533509cf79f399341ee6e0aba367bc","datavalue":{"value":{"entity-type":"item","numeric-id":5394151,"id":"Q5394151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84e1cd72c2268dd03dc433e01a81b936733c9d3e","datavalue":{"value":{"amount":"+0.770313024520874","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":"Q1404980$C9500665-FFA5-4F3C-B1E0-9E8652A615F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1d683ef670cfe0396ca25a3659cc0c6554128d7","datavalue":{"value":{"entity-type":"item","numeric-id":4539640,"id":"Q4539640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b15fa3465caa8804f641a5ad50147ea23550935","datavalue":{"value":{"amount":"+0.7651974558830261","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":"Q1404980$D38ABD6D-0AE9-4034-85AC-DB191428FB9E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Depth-first proof search without backtracking for free-variable clausal tableaux","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Depth-first_proof_search_without_backtracking_for_free-variable_clausal_tableaux"}}}}}