{"entities":{"Q3067537":{"pageid":3078253,"ns":120,"title":"Item:Q3067537","lastrevid":86309816,"modified":"2026-06-03T18:13:46Z","type":"item","id":"Q3067537","labels":{"en":{"language":"en","value":"Satisfiability solving and model generation for quantified first-order logic formulas"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5839899"}},"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":"Q3067537$14895709-5167-4F11-AB24-B998DA8BF487","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e2807d5983f929caa09e9d5cb44142cb68e47d57","datavalue":{"value":{"text":"Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3067537$DB7948F2-C843-4BCC-A8E6-376DA2BAB7B6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"296df9c676b4814370616ffd54f17ccf6300bd45","datavalue":{"value":"1308.68039","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067537$0DACA901-1A2A-4530-94FB-790D85DB7953","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"465ae614934f426173873f90f19e53d99b9dbc40","datavalue":{"value":"10.1007/978-3-642-18070-5_6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067537$1CCD45D0-59B7-4A84-85AF-C8541B9325E4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a068b9147c7234de85f0117b92e2136cba8ddab2","datavalue":{"value":{"entity-type":"item","numeric-id":3067536,"id":"Q3067536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$6AC7E671-B189-4080-A4A8-54A05CDFFD64","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"dc79f3ca1ff011706d97e4cc9dcb7a33f54133f7","datavalue":{"value":{"entity-type":"item","numeric-id":3067528,"id":"Q3067528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$2A6D003B-AD1B-449D-9AC7-E8CAA82ACEEF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3832aa8c4413a9f491fedd54c1d4e68094c46118","datavalue":{"value":{"time":"+2011-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3067537$1C84EA2D-C374-4E38-BAF1-3ED11F98F303","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067537$8BAD8CAF-48D7-49DC-BAF9-1D992111596B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067537$D1623DA7-0A55-4B7C-8A35-A6CD04257660","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067537$76F2ADF7-29CB-47DE-BB57-74A930E96B84","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cb27a1ebcb53123feca90133b3032b1ae5d1edd6","datavalue":{"value":"5839899","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067537$08C4DBD3-6D47-4037-BB09-EC5B72E94109","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$33BF9B3D-D946-4BDA-9BED-FCEA254A46F2","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":"Q3067537$78ADBD9D-E34D-4BB8-8DFF-6CAA04668864","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$5F330147-7464-4116-B4F6-D972D0718461","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$1AE27902-97FD-4F42-9751-A1EA594EA2D2","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":"Q3067537$B4C3E44E-7DE8-4610-8922-9D5C130E234C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a49d0bfb2688a5b347a587b284208f2474459736","datavalue":{"value":"https://doi.org/10.1007/978-3-642-18070-5_6","type":"string"},"datatype":"url"},"type":"statement","id":"Q3067537$6BB3A777-5B12-474A-AB63-BC8E92F625CE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"21941fffa5d23f48412dd2c6c720d3bbaa016536","datavalue":{"value":"W1579447681","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067537$39787122-071A-4853-8AC5-6FAB0AECA034","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a707b674693ad1e1d950930d4096a03ee1af3ca","datavalue":{"value":{"entity-type":"item","numeric-id":4472553,"id":"Q4472553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$9AD9653B-1EEF-40B9-B3A0-C39D61994049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$B70C9FD4-1234-4DCA-8F4E-A1669CDACAB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7cd2a25d693a4acd921e56f15d1b3d06cb750f8","datavalue":{"value":{"entity-type":"item","numeric-id":2754081,"id":"Q2754081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$6B536147-5325-40D6-B981-6AAAE65EFC53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$3237F88C-1CE8-4870-B926-6754E71B8BC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$7166AE7A-09CC-4789-B7D5-684967CD2446","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"90d27466745eba57837a04b18173a99a47f5ad2f","datavalue":{"value":{"entity-type":"item","numeric-id":1037401,"id":"Q1037401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$91B07D71-11FC-482D-8924-C089E3B7CF31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f426d61b5e73f09c762af22502a76e1d6d446b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$3EA40763-5416-43D7-B584-1551A542A9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d20b8831971314127eaeeb3efdaae0475c97a8fe","datavalue":{"value":{"entity-type":"item","numeric-id":4916219,"id":"Q4916219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$536FD12D-1F67-4FCE-B997-4753D8841551","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":"Q3067537$064CB045-27D7-4FAA-B4FD-3B475622C869","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2790188d3a2572a99d3b8280868598d27c040965","datavalue":{"value":{"entity-type":"item","numeric-id":4525781,"id":"Q4525781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$A7BAD2C0-6730-44D3-9796-9EAEDD972641","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c4d8e42945beda42154d7aec024ac2937b8249c","datavalue":{"value":{"entity-type":"item","numeric-id":2864401,"id":"Q2864401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$CC37CE96-6327-4BA7-86A7-44EC30F98AE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1eb2c7fe3771565da9701c0fc3df1bd444668f","datavalue":{"value":{"entity-type":"item","numeric-id":5432330,"id":"Q5432330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$662498EF-AED1-4849-8319-A9A85F8581A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f0b555d657cb1f5a17dad4f6c65786062114626","datavalue":{"value":{"entity-type":"item","numeric-id":2487870,"id":"Q2487870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$2AA71597-C439-4430-A70B-411B73ACFACF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9b6bedea1cffabec2896430aabcdd08d9b551a1","datavalue":{"value":{"entity-type":"item","numeric-id":5387908,"id":"Q5387908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$E0F00EC8-0EDA-4A85-878F-80FB16FB9A4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc23141dc84e97827108c755d4336b0d5851beef","datavalue":{"value":{"entity-type":"item","numeric-id":5423862,"id":"Q5423862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067537$A7EBAAF6-6EEA-4196-B9EF-1544CC25D208","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2cdf6bd8a99dda6fb6242ab5c5bc700cb0b914a7","datavalue":{"value":{"entity-type":"item","numeric-id":6039409,"id":"Q6039409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ba80f0a3b196f7ba1e0c030d12f21126ae6f8aa","datavalue":{"value":{"amount":"+0.825620710849762","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":"Q3067537$946FDC61-F54E-4FEB-9A8B-F96F1F030C42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ef4d4de289000e0b726d89ac0d7d5d3c7e3196c","datavalue":{"value":{"entity-type":"item","numeric-id":5698259,"id":"Q5698259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c05fc7ab4aa6a14371b28833ce45b3a715c9f25","datavalue":{"value":{"amount":"+0.7959665656089783","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":"Q3067537$7EDC4D9B-1048-4868-AD17-A82A7F513F7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12aaa4a36bdf05dc06c575e9e83887fbf42b685d","datavalue":{"value":{"entity-type":"item","numeric-id":1037401,"id":"Q1037401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d0f3452d8b2c160face425b43cbe148cc313e35","datavalue":{"value":{"amount":"+0.7694233655929565","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":"Q3067537$7472E0B1-E09E-46FF-B7C9-7D7460E75E01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9390b4ccc6dc9f08d9ed8cd2d7f1eed1c352e9ee","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb734f8e2c973448b19ec750d2f0e3b6fa9eb1eb","datavalue":{"value":{"amount":"+0.767562210559845","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":"Q3067537$97AAC5A1-0C81-4F5C-9C6D-64E2449EBC26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a321b69eb32f47eec245538b125547d32b51872d","datavalue":{"value":{"entity-type":"item","numeric-id":4593094,"id":"Q4593094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05d963ae38051abcba8a227f20088143d18139ff","datavalue":{"value":{"amount":"+0.7436672449111938","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":"Q3067537$603E714A-7996-4D5E-A5BC-E06E3B3504FF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Satisfiability solving and model generation for quantified first-order logic formulas","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Satisfiability_solving_and_model_generation_for_quantified_first-order_logic_formulas"}}}}}