{"entities":{"Q438540":{"pageid":440307,"ns":120,"title":"Item:Q438540","lastrevid":61924455,"modified":"2026-04-11T02:35:12Z","type":"item","id":"Q438540","labels":{"en":{"language":"en","value":"Automated inference of finite unsatisfiability"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062050"}},"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":"Q438540$34158BF8-86B6-4F38-AC9D-AFD46D5BF522","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8cfc2960fa4cbe4615aa9c2075c431afa478ecbc","datavalue":{"value":{"text":"Automated inference of finite unsatisfiability","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q438540$D52A5275-7906-4ADB-BA62-56F9B683BDF0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c7b7b17c8525a85f4182e38168677f1b502e6606","datavalue":{"value":"1243.68266","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438540$5A4BBB69-442D-4DC8-94B5-D3D67E80C5A0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1ebcb9f6003248d9f6e3888a3874f451e22b906b","datavalue":{"value":{"entity-type":"item","numeric-id":438538,"id":"Q438538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$CED14F5B-613F-4D1D-A1C8-8E250D5C25DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"98813b9f434f6a88bc404ff2ea2f8e4c67626ae8","datavalue":{"value":{"entity-type":"item","numeric-id":438539,"id":"Q438539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$6EA25199-420A-4A8F-8FD4-100AA99F53E2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$179800CC-7150-4275-816A-A862252000C6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q438540$C8B84C55-FDE3-467E-BE71-8469CD1E955B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438540$3B3E3DF5-42B3-4838-BC99-126A328D91C9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"16036da7dca95425fd2891a3aadfeffb2accd604","datavalue":{"value":"6062050","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438540$DDB55E38-C5FB-408B-B82E-F8C94F62A65C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e226d10f64c07d4c4a119587c41dc31e161f2478","datavalue":{"value":"finite unsatisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q438540$EFFEB851-341B-4583-B16E-289668BF9E49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q438540$79AE8CC8-02CD-4A93-B935-CB339E0EC7D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q438540$2BD3AEED-7A52-4C0C-9A8F-CD1FC5FEEA19","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$0484029E-C2CE-4E23-8A41-0DC11DBE607C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$4DD4A40A-6E4D-4481-8E88-A8AA14B46D7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$AA5E278E-0FDF-459B-9815-03A086106634","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$D7B95DFF-C53C-40F7-8CBD-E6E6C34B8AC8","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":"Q438540$18883F8C-D906-447F-A85C-851D44862467","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6e92e4d1be93f27837961f960a6ff910e855fe09","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9216-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q438540$758198DB-E625-45D1-B492-24D2F2D4E8A1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2253047c18ff885b6f528c14db10219a3440b892","datavalue":{"value":"W2079943511","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438540$A89EC7DB-1B4D-478A-A0FD-0A00F9B73CAE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4adc22ed174f33297ffa675f67b5ee27a98ff71c","datavalue":{"value":{"entity-type":"item","numeric-id":3541699,"id":"Q3541699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$D91B7BF4-494E-4697-B19D-9D203314F067","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec28c2a46c17d6b0806fc14a11fc75ffc107a63d","datavalue":{"value":{"entity-type":"item","numeric-id":5191115,"id":"Q5191115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$214AC40D-0565-4AE4-91B7-3025BBC94E5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1845121d7204a561acfbb8b55f7d2a361a55e0f1","datavalue":{"value":{"entity-type":"item","numeric-id":4178997,"id":"Q4178997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$7E738C6B-5064-42CA-AA91-A00A6814712F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0c51e24e1428721a6903741aba45a8914c5f370","datavalue":{"value":{"entity-type":"item","numeric-id":1373299,"id":"Q1373299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$660F1379-8945-4843-8537-4185B018AE5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$FBC2A495-11EB-4EAF-B07F-290D150EE63E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$28CC6189-FD69-4DC0-8425-6C68388BB98F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66ed1fd88663850940208777b453a5e31171f5d4","datavalue":{"value":{"entity-type":"item","numeric-id":5486135,"id":"Q5486135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$EC777A94-5171-470F-8EEA-EC7AF91B920A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f49bddd3d8758939d2c56cea336fa15d4d01af13","datavalue":{"value":{"entity-type":"item","numeric-id":4809064,"id":"Q4809064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438540$4ED62023-18C2-47A8-A82C-62BDBDFC6710","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"40c9e335fef54047d3e19301a8f299c476d5632f","datavalue":{"value":"10.1007/S10817-010-9216-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438540$1BFAEA9B-C996-42DE-85A4-D256F5F2CAF3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1ef07658f5d1bd9482fc3ffa2ee4d0683a3a2b1","datavalue":{"value":{"entity-type":"item","numeric-id":5191115,"id":"Q5191115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b207f73ad7526d6df9a79fe90659ee39d5ad7bd4","datavalue":{"value":{"amount":"+0.9949392080307008","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":"Q438540$003364FA-3DA3-451C-B801-2E66DC3825AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cefb701784a16939bba13f30dadcd92d23de286","datavalue":{"value":{"entity-type":"item","numeric-id":5505496,"id":"Q5505496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4470867d516cebf5a0233dc318869f1db47a6aa","datavalue":{"value":{"amount":"+0.7367056012153625","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":"Q438540$FC4C6080-EF65-4F1C-B1C8-2726F7A12220","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c67c8d20ae5b9edf979a7ab3a91e204c0ee550d4","datavalue":{"value":{"entity-type":"item","numeric-id":3192187,"id":"Q3192187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a05ba0b2d4649a531ebf2d1d1fd534972542860","datavalue":{"value":{"amount":"+0.7327504754066467","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":"Q438540$C0CA5BD8-7938-406A-831D-745A66F00749","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e14787651e93bfe1fa0ed3046e7a940302c5a5a","datavalue":{"value":{"entity-type":"item","numeric-id":2281661,"id":"Q2281661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f9b7e55863ae2b7f45a530ec9b0dbef0f70ba7d","datavalue":{"value":{"amount":"+0.7260493636131287","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":"Q438540$943EDA79-6A6C-4BC4-B530-7D7EAA665DB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f6d087bc689afa181873c6e1fdc2d092ef94a025","datavalue":{"value":{"entity-type":"item","numeric-id":4209295,"id":"Q4209295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"506e82697e125511d0cb13c0189e0aaa2bf315d6","datavalue":{"value":{"amount":"+0.7056564688682556","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":"Q438540$D9618E86-D78B-43D4-A070-75A14C2985F3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated inference of finite unsatisfiability","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_inference_of_finite_unsatisfiability"}}}}}