{"entities":{"Q4247076":{"pageid":6276677,"ns":120,"title":"Item:Q4247076","lastrevid":41257506,"modified":"2025-04-25T11:23:49Z","type":"item","id":"Q4247076","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1301853"}},"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":"Q4247076$A6C5A078-26AF-47E6-A415-E4B87C1D6FD7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2c062042adeb6aeba3154d754fb0a7b558902433","datavalue":{"value":"0930.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4247076$94CA4C33-D7A8-4ABC-8C49-4316AAFBBBB2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8b5bfa12347d4716af416e8493dcfe0d9b94cba5","datavalue":{"value":{"time":"+2000-02-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4247076$66446818-B474-408C-A041-95C09A7668FD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4247076$F9BEFED4-F34F-4D83-A295-B9383EFB3995","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"abca938afd309309893053e8ee4f51374fed9de6","datavalue":{"value":"03C07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4247076$A578D2FA-24EC-4418-8B29-3620D1943F40","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d4294e5ede44cb60f6f620ce0a874b6fff94d398","datavalue":{"value":"1301853","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4247076$D4B5B34A-51A0-448A-ACE3-54266C7E63CE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b02c1076ddf1832bad611618549cfbe8e51921d3","datavalue":{"value":"HOL Light theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$6CCE6B19-7BB9-44A2-99AC-255B7FA66253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c4ed4fea13432d188a5ec678aec936f44975a8a","datavalue":{"value":"syntax","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$912B8C90-5AF0-4356-8206-1B114DAFA4BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eeaa93e2a77f12f86d8529a6c6a9ffaeb6f16c80","datavalue":{"value":"unsorted first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$7DBCBD55-0F00-403C-AE91-674574D9D92C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1bc362a3d23ead7ad61faf33b274da9ec769cf80","datavalue":{"value":"HOL datatype","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$4AEC53D3-C770-4765-95EA-AA28AA987780","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$288F520F-EC3B-4D9D-8879-1DA4A9B11DB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b57c832f4b21b0ae9151495d8a971f39ac6c1824","datavalue":{"value":"validity","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$D91CE51C-0865-4F98-8B63-F450F7E7B4C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$D5F0D65A-5B99-44FB-987A-FB8CFEE3DA42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"64eb0526ddd84dbb542616b90ad41b6b0bac8bf1","datavalue":{"value":"Compactness","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$3EC731E8-9869-4364-9AB0-D8417B1E7CE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ede2c71c63a79d3e8d20236d8634948a63d9882a","datavalue":{"value":"L\u00f6wenheim-Skolem","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$B06BD2AF-93B9-4A30-865B-9BA37C268E8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eab48424c633c8ea6348681e2181ba2c9be99089","datavalue":{"value":"Uniformity","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$B8F6C28C-4D79-4364-B67A-64AAFEF2E447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aa8cefedabe6795ed44a4f59368d0ce4caa3e7ec","datavalue":{"value":"canonical term models","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$63652744-650C-4C69-94EA-7A0C7934E3A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b34e81c9be74c25aae2603a8dfa343c349c2721","datavalue":{"value":"Skolemization","type":"string"},"datatype":"string"},"type":"statement","id":"Q4247076$374595E7-E657-4F59-B6C6-E83F30BDBE99","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4247076$BEB9D7B0-52F6-4763-9121-12D1D95C3E8B","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":"Q4247076$DB34B0CC-10D4-4FB0-8904-1CBEBE8911C9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1841c0107b8bdc2b59e43c2e2095aaf7f436a891","datavalue":{"value":{"entity-type":"item","numeric-id":4305337,"id":"Q4305337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e83e4b8d1fe9d26d300d97edccfe66589ba02dcb","datavalue":{"value":{"amount":"+0.9214801","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$9C814935-47D4-4611-9023-EFD6B01643EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85445e218d9c7de34710abeb0c0c4584e4d8d5dc","datavalue":{"value":{"entity-type":"item","numeric-id":2865746,"id":"Q2865746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b38be8b6411cbddc1e77cf34b10261859b8a579","datavalue":{"value":{"amount":"+0.91991603","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$24D4F4DC-45D5-4193-AD3D-9CFEA33C14CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"518f113214d8dacdfd65ea5ea7302a8ee399d9bc","datavalue":{"value":{"entity-type":"item","numeric-id":3075243,"id":"Q3075243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa0a6143d8bffa1ad0148a4b9b4fda3691fecbad","datavalue":{"value":{"amount":"+0.9191854","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$A88293A3-38A4-468C-9E00-8A8400E8383E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"526a32793d5d654226901c97b2a231f0c768efe5","datavalue":{"value":{"entity-type":"item","numeric-id":5275277,"id":"Q5275277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b25f4b2045145cd8c81654d1280f70220151dc81","datavalue":{"value":{"amount":"+0.90792286","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$C2FDAF24-E88B-4D68-9E30-7B3ACE33254A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"168f003cce15db30adfa93966a4178bec2b81617","datavalue":{"value":{"entity-type":"item","numeric-id":5687548,"id":"Q5687548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"186b184cb98a038f7a7e426780660d529d4db5f8","datavalue":{"value":{"amount":"+0.90571404","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$5B947D6A-1BBF-46D5-8B42-8E48E06D4019","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b46c44a0ee4845274d77cde09d6195438061a3c0","datavalue":{"value":{"entity-type":"item","numeric-id":4944337,"id":"Q4944337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4fba1ccbf4402b616ae3446eee6af0226f0e1e9d","datavalue":{"value":{"amount":"+0.9050228","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$A5686CB8-ED0C-433F-B323-F6403DAD4A73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"336a295948b4612660cca8cf7bc92751b55f83ec","datavalue":{"value":{"entity-type":"item","numeric-id":387121,"id":"Q387121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df75cf1520e83437f0bd2b02487d94c4e5ffc997","datavalue":{"value":{"amount":"+0.8981217","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$F08A2293-EB4F-479A-B22E-740DD60894C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92cf4a098c4740b58a63a324276145b1e9ddbc66","datavalue":{"value":{"entity-type":"item","numeric-id":4028090,"id":"Q4028090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb342587e52652b0593ccde5da1941faf36d38a4","datavalue":{"value":{"amount":"+0.89654094","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$3ED72F05-022A-49ED-B966-C485886E0556","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2cffd5ebf8dfa9639887aa1690f633bf306f8c7b","datavalue":{"value":{"entity-type":"item","numeric-id":2945706,"id":"Q2945706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"514fbcd303d1027648ab9543a6de170f5b6f2779","datavalue":{"value":{"amount":"+0.89289606","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$088F48AB-C84C-443A-BF55-32321893C12F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e5172a92f343de86c9809e312fd2211d411a7d7","datavalue":{"value":{"entity-type":"item","numeric-id":2964455,"id":"Q2964455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f4e3213c10143ad6fe98b88a148addeb5dd43ae","datavalue":{"value":{"amount":"+0.89282876","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4247076$F04F0728-0BB9-410E-B587-239496017687","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4247076","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4247076"}}}}}