{"entities":{"Q3088006":{"pageid":3098721,"ns":120,"title":"Item:Q3088006","lastrevid":45420994,"modified":"2025-12-07T17:47:46Z","type":"item","id":"Q3088006","labels":{"en":{"language":"en","value":"Proving Valid Quantified Boolean Formulas in HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5940068"}},"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":"Q3088006$EC9C95C0-938F-4AB2-9D60-726CBD31D95D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9a87e61ef26d07f666c0e2f0624f00acba711e26","datavalue":{"value":{"text":"Proving Valid Quantified Boolean Formulas in HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3088006$E736D6F9-7B23-4F55-ACFF-94070CD928BF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"044f6a8bba2989d2005b2193ef6f6ebd8728695c","datavalue":{"value":"1342.68291","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088006$11C63BAC-4692-4245-9A62-15BA543A5719","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a9c8e5335c34ee45de80fad990193735900c1c0f","datavalue":{"value":"10.1007/978-3-642-22863-6_15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088006$9C90187F-1154-42DD-A969-68D20F739582","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb18cf0542c9d5785b9c3d13ac135abc8a7efb68","datavalue":{"value":{"entity-type":"item","numeric-id":1687532,"id":"Q1687532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$1A008F80-6951-4736-ADC1-C369347024AA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$B2E2A61F-441C-4906-BCFC-187BD931F427","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cf253edeced6fad2edf52e73f99001914b4fc105","datavalue":{"value":{"time":"+2011-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3088006$7C47ECB1-7656-434F-BE60-B39125D68A9D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088006$1AE4C1AC-29D7-48EE-BDD1-5B9E161B4675","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bc4b288f525c7080f6f92f36e11f9beb32026b67","datavalue":{"value":"5940068","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088006$668A50BD-270C-44F0-969F-D40C6A3D8285","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bf8fe40ec0751f683b8f31fdc6f7f38f8aa07409","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$6BBB0A46-4BA3-4985-8B34-1BE2B0A53736","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$BA1F59A7-1749-4F53-9B9B-3C8398E7463D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$746AF2F4-926E-4438-BDFA-B016C12EBEFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f81f218aa9dfbe89c11e108de13663cbf6e414fc","datavalue":{"value":{"entity-type":"item","numeric-id":21436,"id":"Q21436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$4551510F-E865-4BC0-BAFA-E1A06843C4DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$55A8B22F-3B52-4D57-B3AF-878768DB3F8B","rank":"normal"},{"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":"Q3088006$EF9D8CBD-9404-4CE8-8C07-38F3C218B202","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":"Q3088006$B3B91199-C5AB-4DDE-9CAC-DBDE555D04B8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2e9f73d08550c20b370be101dd7d8f175dc036f5","datavalue":{"value":"https://doi.org/10.1007/978-3-642-22863-6_15","type":"string"},"datatype":"url"},"type":"statement","id":"Q3088006$4B8F2B21-8E6A-4618-944F-D16BC22B8075","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"bfe18fbbae6aafe0eebb5c5e2b51eb80d46f7dda","datavalue":{"value":"W152437424","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088006$5A423A77-0E26-46AB-A084-D4A36AA8B116","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a602a31ec5858953936704adacfb1f5bdcaed350","datavalue":{"value":{"entity-type":"item","numeric-id":972422,"id":"Q972422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$9C1E311F-6A2F-4C80-8829-242DD7FAD14E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ebd47a55b9c2aed7b10858aad59c96098e81642","datavalue":{"value":{"entity-type":"item","numeric-id":3620436,"id":"Q3620436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$3942E463-1CE2-488E-BF29-A14121A74018","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$A238560C-8BC9-4B2A-BDA8-F15B70939370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4dec1714ca604e89b31baf4ac49a15a60cdb203","datavalue":{"value":{"entity-type":"item","numeric-id":5712370,"id":"Q5712370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$D75E735C-B658-4713-BB58-0C265941655A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0870e13c4a5dd2b1ec6ccf0eb8fddafbaa000d2","datavalue":{"value":{"entity-type":"item","numeric-id":5713732,"id":"Q5713732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$FAFA449C-922E-4B9C-99B4-AB07690AD089","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"733b26423c0997d935ca2ea4b4cf0e3d6ed48386","datavalue":{"value":{"entity-type":"item","numeric-id":5714777,"id":"Q5714777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$39AEC4C4-16E4-43B2-A7B6-6ED3DF3E3E36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeedc506ee95714a79cfc16f82862182df8774bc","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$AF03ABBF-DAC0-4988-B56F-D4E08AC6B601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e5d997d3c3c1c4cbe0d251137694980cd98cf08","datavalue":{"value":{"entity-type":"item","numeric-id":1272607,"id":"Q1272607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$B9610AC2-37C7-450E-8E2C-F6DA8E777593","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a693c10013eb7bffb7ffbc0c1890644cc6a21fe5","datavalue":{"value":{"entity-type":"item","numeric-id":4809048,"id":"Q4809048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$8A4070D7-7DA8-4076-976D-C4AD271C3538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e81867e3920d63292ec40a953a0141bb46dbbec3","datavalue":{"value":{"entity-type":"item","numeric-id":3612467,"id":"Q3612467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$E08BFC8C-AA2D-4E50-88C9-0879D50401E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f38c339bbd571c9f13a1b3052c0abde7b640b4a","datavalue":{"value":{"entity-type":"item","numeric-id":2471742,"id":"Q2471742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$1DD379E6-F19D-44F3-A06F-404211758CEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f33f843778dfabfeef453cdfa627d4b42c24908","datavalue":{"value":{"entity-type":"item","numeric-id":4131648,"id":"Q4131648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$BF426775-8E59-4246-9E55-58885528E624","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"241a84e6f61ddf1a88ab9e24d91b0723d27a5775","datavalue":{"value":{"entity-type":"item","numeric-id":3400890,"id":"Q3400890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$F652AE7B-727E-40DD-AA8F-55CE8A9D8439","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"716d170b6d9b095492bf0c2b742ee0dbade5bbe0","datavalue":{"value":{"entity-type":"item","numeric-id":3523178,"id":"Q3523178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$843F53BC-201E-4FE3-BDE9-A5E575C12A64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ea3f027a8a8102e42a9169d39f304a1180d2fa1","datavalue":{"value":{"entity-type":"item","numeric-id":5747670,"id":"Q5747670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$5CFA7FE6-DC69-4250-8080-964CA741E149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088006$98479FFB-46E7-4640-94CF-99314CA65482","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"297d7ca756a0fe9edb01e6c2d45d7d8ced12f185","datavalue":{"value":{"entity-type":"item","numeric-id":3088005,"id":"Q3088005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4ff664ae8210c6006b3276a17c97a28de44aa92","datavalue":{"value":{"amount":"+0.8863806","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":"Q3088006$EB8DFB41-DB8B-4581-9AF1-B7881A31C1E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21bfa3d98839930151ea0a383eb5107129ac8562","datavalue":{"value":{"entity-type":"item","numeric-id":5747670,"id":"Q5747670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99b448473d43459a9744e264321462b7638c3a92","datavalue":{"value":{"amount":"+0.88348615","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":"Q3088006$5A81B6D9-622B-41A3-8EBB-10F4DE61E74F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30852398fefb28081892de18f8d5a4275b4e5662","datavalue":{"value":{"entity-type":"item","numeric-id":6050769,"id":"Q6050769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e726dacb8e50b263eb9e0ee3924f86a12f33ea3d","datavalue":{"value":{"amount":"+0.86535823","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":"Q3088006$D6AE9B55-A1BE-4C54-BD5C-45DD0FCF7C19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6397715b4b253111073a53ff394cddb3612a19b9","datavalue":{"value":{"entity-type":"item","numeric-id":1408385,"id":"Q1408385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36133a43de83b46460f3154e70542d8728c5559d","datavalue":{"value":{"amount":"+0.8634523","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":"Q3088006$E42B1D05-C1F2-440F-839A-D866257A4E67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"468f7da087c5780388f6f08ecc01b3e3bbd67087","datavalue":{"value":{"entity-type":"item","numeric-id":4489064,"id":"Q4489064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32e7eca2c410f75c09cc8fb0af6de62883013cdb","datavalue":{"value":{"amount":"+0.8633928","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":"Q3088006$E85640D9-A501-4303-923C-1CA34936054C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab683a7b1f35576127c529e6651dcc1403e6eaef","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"226390863ad344867f9974292f197d73367a7fc2","datavalue":{"value":{"amount":"+0.85947585","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":"Q3088006$AD8F48CB-F1BA-4552-B46C-7D12BCAC806B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0987db3ffa1a6ab311eb02ef5c2d1e2ebf46c128","datavalue":{"value":{"entity-type":"item","numeric-id":1045994,"id":"Q1045994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eafc01d9e71d5f6870a5c132caf641327ca8bc7a","datavalue":{"value":{"amount":"+0.85552394","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":"Q3088006$C138E13D-782F-45FB-BC83-EDD06A36CAB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6faf0a10ebac71dec9e2a37741b5ded2bec96e0a","datavalue":{"value":{"entity-type":"item","numeric-id":2435315,"id":"Q2435315"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a25118726cfce0258c5dbd80099d8226917aeefc","datavalue":{"value":{"amount":"+0.8553439","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":"Q3088006$EB375F0D-D6FF-46E6-8C3B-32AFDBBB1C8C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3088006","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3088006"}}}}}