{"entities":{"Q3000661":{"pageid":3011385,"ns":120,"title":"Item:Q3000661","lastrevid":51248876,"modified":"2026-01-17T10:55:53Z","type":"item","id":"Q3000661","labels":{"en":{"language":"en","value":"The ACL2 Sedan theorem proving system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5897416"}},"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":"Q3000661$14BE4333-EEB3-4823-ACCA-0447F11CBFEF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"87dc752dbaa94c02c70a86b0c8d93bb1da78d877","datavalue":{"value":{"text":"The ACL2 Sedan Theorem Proving System","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3000661$9A27F674-6899-4FBA-8447-85866BF30F23","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4693d306ce99723c3882debed1dd36678ac2e5ee","datavalue":{"value":"1316.68132","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000661$079C799E-B196-4078-ACC1-7D9FDE0EC0C8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6eba75b426efca5f095341c8ea6c846fa07b320d","datavalue":{"value":"10.1007/978-3-642-19835-9_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000661$814EF2DA-EBC6-411A-A55C-D34AC2F238D6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"be9924a236eb2dba629918cc14b9caf078368acc","datavalue":{"value":{"entity-type":"item","numeric-id":3000660,"id":"Q3000660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$627AB7CF-E3BD-4FFC-A037-4AF895C0D57E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f3524b9c32b1166213486322dd60fbb6b441c057","datavalue":{"value":{"entity-type":"item","numeric-id":2867931,"id":"Q2867931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$EB465657-AD6D-4CE8-820B-AC65D9417518","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"07ef5bce62b88cfecff16603e8667fcc383b0d99","datavalue":{"value":{"entity-type":"item","numeric-id":479822,"id":"Q479822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$BDC09F01-59E7-4DFC-A0E5-8EFB1DB062F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"49a02d2967366c05338e9a85c6a94315b1ebf4a5","datavalue":{"value":{"entity-type":"item","numeric-id":851143,"id":"Q851143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$1017CA4D-415F-40CD-8FB1-3D3A44D4D65D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$1B3A81E6-EF89-4AF5-82EB-93B2D5ABC3C3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"07154ee076353c2b0adec8e531d763756f4412f7","datavalue":{"value":{"time":"+2011-05-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3000661$7E546862-006B-4316-BC08-0D7F6C48B430","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000661$710F83A6-7549-4407-9DFB-E0F299162E8F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cb6adcdc5e900b420f7b196e03890e262bd7cb4b","datavalue":{"value":"5897416","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000661$60364F29-0926-4E48-8B94-A9BAC7823AA0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$8C50C8E3-2596-4C91-BA82-CDDEB17262B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6a5699a860dd7dc9c732976be3ba437fb61ff7dd","datavalue":{"value":{"entity-type":"item","numeric-id":19322,"id":"Q19322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$860941B1-BF76-4E9F-A336-577260030EF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f1efe251f10f20310d9fc2391ac64c314c66eb36","datavalue":{"value":{"entity-type":"item","numeric-id":19751,"id":"Q19751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$59DF080E-C5E9-4FB4-8A3E-191497EC0D97","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":"Q3000661$C5B09267-456B-42F1-A6D9-2AFBE0075B9F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2bf8d0af33cfcae85464c0d2ec8ff55539084e67","datavalue":{"value":"https://doi.org/10.1007/978-3-642-19835-9_27","type":"string"},"datatype":"url"},"type":"statement","id":"Q3000661$3BCF818E-43B2-4C49-A960-5C195D495C21","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8dfe0c0d97698bd937ac474e3d8343a8d3c4a024","datavalue":{"value":"W1727725625","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000661$862CDD41-D813-4179-8995-F9B7C27EE5FC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8ab3e683fcf1f4589adbbb54eed5465c20ce3fa","datavalue":{"value":{"entity-type":"item","numeric-id":2867932,"id":"Q2867932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$3DB3E7EE-F2A7-4634-92AD-270B87F08D74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ffe62377108373cd046811a24014b149bc79d51e","datavalue":{"value":{"entity-type":"item","numeric-id":3543644,"id":"Q3543644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$1DE08AA2-DBAA-4ED1-B6C6-2598AC373763","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a71712455a619c09bf3f52fa45ff271444532140","datavalue":{"value":{"entity-type":"item","numeric-id":5756741,"id":"Q5756741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000661$0244A36E-C1CC-409B-9B95-9233BDEE2EFF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28d5a8b545b5823d435e955696d0052fff4439c3","datavalue":{"value":{"entity-type":"item","numeric-id":2867932,"id":"Q2867932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7595a6e2bbc0c6379f62941dfa6f95917c22d247","datavalue":{"value":{"amount":"+0.8985278606414795","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":"Q3000661$17CA8792-630D-486C-8140-0A26E5C4F986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9b7d04a9ff7a9d025be95e1cfc5750dbf6e966c","datavalue":{"value":{"entity-type":"item","numeric-id":3543644,"id":"Q3543644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"adbd2b7f300845a926b87c4b702334df819e9900","datavalue":{"value":{"amount":"+0.8269709348678589","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":"Q3000661$AD81F9B1-AB28-44D5-BC19-9FDC38488F57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b3b0efa447d2f0bb1d07cfcfcea727ec3cbe250","datavalue":{"value":{"entity-type":"item","numeric-id":2280212,"id":"Q2280212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31ac5a64e5afa82ba85e3c4a964dad91f71095f7","datavalue":{"value":{"amount":"+0.7776650190353394","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":"Q3000661$91C572E1-FDC6-44AD-B183-C442A067EBC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15d76b42d1c936c5ae7793777e9f9178a1e4946d","datavalue":{"value":{"entity-type":"item","numeric-id":5083764,"id":"Q5083764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a25c56705a52093a7c9dec313647287fcbd139b7","datavalue":{"value":{"amount":"+0.7640705108642578","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":"Q3000661$A3731A3D-15CD-4985-B47F-048D8A3E5096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9c7e2906cab0df39eaaaec6ded4334d15f17931","datavalue":{"value":{"entity-type":"item","numeric-id":4471942,"id":"Q4471942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3eaf6cb6d4ee6994537f3699185bd3a1c2d474e8","datavalue":{"value":{"amount":"+0.7445371747016907","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":"Q3000661$5D2D5F2C-D6D7-46AD-9718-8EE65CA7F2F6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3000661","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3000661"}}}}}