{"entities":{"Q1601865":{"pageid":1612605,"ns":120,"title":"Item:Q1601865","lastrevid":67960500,"modified":"2026-04-12T20:29:47Z","type":"item","id":"Q1601865","labels":{"en":{"language":"en","value":"TAME: Using PVS strategies for special-purpose theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1761179"}},"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":"Q1601865$68B28CD8-764B-49C2-B743-C288E24915F4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d640083053e12e6d72077009719f2150600c6d38","datavalue":{"value":{"text":"TAME: Using PVS strategies for special-purpose theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1601865$B266846E-55ED-4225-A995-A02E31082DE0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6e1ef57347cdda914f80c0f46d83dc0ad4294d6b","datavalue":{"value":"1001.68127","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601865$D9BE963D-1361-41AE-ACE4-466223949CA9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"aed5447785366daa371a0b048f0086d3a34e9002","datavalue":{"value":"10.1023/A:1018913028597","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601865$E5DEFF49-E59C-4319-A438-D5B0AEB3B1B2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7346dc34d1d50fea46ec345fbc7e3214530889ab","datavalue":{"value":{"entity-type":"item","numeric-id":276517,"id":"Q276517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1601865$23C56BEB-82AB-4821-AF1F-F2B0D3D77068","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6aa0b5839eb2d6e7fb371f8a4ca03238e6998f63","datavalue":{"value":{"time":"+2002-06-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1601865$C0E4244C-8DA7-4F27-9F97-52AA20C92120","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601865$FC6A29C9-3FAA-48E2-AFEE-06D2D78A4C78","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"facfae92033afad3c811fa4f2af66bc3ddf44934","datavalue":{"value":"1761179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601865$CA9F23E3-F1FB-4B4C-800F-8B3752D608F9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601865$C4073BDC-0319-4295-9CA8-A87169533301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98b5b5a4f0c825ea91b5dc8ad46045a364b8968b","datavalue":{"value":"strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601865$A244523F-E4B0-4BF3-8880-EA16B305AEB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601865$E716DD67-A093-402A-96A1-52C577CF52FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b5b7d16aabed335eb206b31ae015d3b380be1a73","datavalue":{"value":"timed automata modeling environment","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601865$360EFD02-2B88-4C36-879B-E5470D4166A2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a5e7f34f5647aa6603bde54bf3aa46d019e1c75","datavalue":{"value":{"entity-type":"item","numeric-id":633294,"id":"Q633294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1601865$0AD55EEA-1B23-415C-B34D-6EC53E7629DB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6b29ece733eca165d3fe96eca18b072d2b1513b","datavalue":{"value":{"entity-type":"item","numeric-id":19003,"id":"Q19003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1601865$3F04DD95-9102-465E-88FB-74268E8BB2CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1601865$B7122A24-56B1-4706-B2E6-6DE450693950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f10e7acb77aa2a053602f0044c4781346f0cbb55","datavalue":{"value":{"entity-type":"item","numeric-id":31444,"id":"Q31444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1601865$46F50865-BB21-4378-A754-23C426EEB591","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":"Q1601865$79BD5320-B387-4BB2-BEDD-96F9B5DC1ACE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"da5dd7e67627586a614620953d8709706cdb87aa","datavalue":{"value":"https://doi.org/10.1023/a:1018913028597","type":"string"},"datatype":"url"},"type":"statement","id":"Q1601865$B3A72BE0-2EE8-4F2A-ABC6-EFD2BB590C27","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aee3fb31a3978121c2cc0ce90274293f2c449a45","datavalue":{"value":"W1870235599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601865$4D5ADC03-D71F-4579-9F6D-791F6BC88E6C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e52c6f724532c9e1142453b70c4782abf07c15fa","datavalue":{"value":{"entity-type":"item","numeric-id":1857285,"id":"Q1857285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d2960979b7dfbbba9f29d9f700716d3ff90b82f","datavalue":{"value":{"amount":"+0.8757774233818054","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":"Q1601865$07D42C66-7DAD-4DD2-89BF-78CA4B7933BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35cb281754ddfbdf132253aa57bc4996b822a6c5","datavalue":{"value":{"entity-type":"item","numeric-id":2848044,"id":"Q2848044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e21a905334b398dc177e5b7992d171d04bd5e749","datavalue":{"value":{"amount":"+0.7766146063804626","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":"Q1601865$127B1157-C0D4-4021-AB27-72D4623A4C08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"742df09458d658ee0759f7fe5f890644f872a27b","datavalue":{"value":{"entity-type":"item","numeric-id":2864361,"id":"Q2864361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a3b2a93bf043afeb41f1c6ebc97eba8a9aedcee","datavalue":{"value":{"amount":"+0.7517549395561218","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":"Q1601865$9E23C06E-BE83-4F40-BD61-9EEF88E5D53E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"899e630ab1ca3ef753087abcf3e220b20d3b893a","datavalue":{"value":{"entity-type":"item","numeric-id":1603708,"id":"Q1603708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"653b00271e50197d460aad52978a7c95ba68b901","datavalue":{"value":{"amount":"+0.7202272415161133","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":"Q1601865$55F3E7BB-962F-4366-85C4-F1F8BEAE7AA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e992dac1bec6dd389398e6ca7adbd355bd13c35","datavalue":{"value":{"entity-type":"item","numeric-id":5897951,"id":"Q5897951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38e69c193792022c3a8cdc1a040a6d40430a9226","datavalue":{"value":{"amount":"+0.7155837416648865","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":"Q1601865$C4FC4A12-BA4B-45ED-8484-023AC0974E6A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"TAME: Using PVS strategies for special-purpose theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/TAME:_Using_PVS_strategies_for_special-purpose_theorem_proving"}}}}}