{"entities":{"Q657585":{"pageid":659434,"ns":120,"title":"Item:Q657585","lastrevid":51398204,"modified":"2026-01-18T02:08:10Z","type":"item","id":"Q657585","labels":{"en":{"language":"en","value":"Automated theorem provers: a practical tool for the working mathematician?"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5996003"}},"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":"Q657585$2329D23C-056C-44D2-B420-1D0AEDC54933","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f24bc3503baaa34d1ef10c6726c25ca04165cae2","datavalue":{"value":{"text":"Automated theorem provers: a practical tool for the working mathematician?","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q657585$30E5FC5D-2CA8-41FE-BA64-368ECB96049E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"337bb4889eb36bedd4d3c7e93996cf4c78b45dae","datavalue":{"value":"1237.68177","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q657585$16FA954C-AF93-421C-A18E-6D4D609BB873","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d37a3d6bd9a0b44736f3bc6a6985f44383a95724","datavalue":{"value":{"entity-type":"item","numeric-id":438542,"id":"Q438542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$69E063E4-5286-4725-9E27-CCC1A17BD388","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":"Q657585$FF38DC9E-8F37-4033-97FE-BBE095737050","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7e9921ac76de2cb0d7fb92248e81ef4146b61b32","datavalue":{"value":{"time":"+2012-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q657585$FC5D134F-6415-4C0D-ADCD-CF0C22269B66","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2acb04531c34893ef4e6c8bf458c124b4be663df","datavalue":{"value":"https://www.pure.ed.ac.uk/ws/files/416060/Automated_theorem_provers_a_practical_tool_for_the_working_mathematician.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q657585$468980BA-C774-4045-8592-10F74246CB48","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"94a8d7a5bc2c46b3b8b9880b7a66b6e0b92f4636","datavalue":{"value":"The author lists some reasons which in his opinion form obstacles for using automated theorem provers by mathematicians and speculates on potential applications of the related work of his group.","type":"string"},"datatype":"string"},"type":"statement","id":"Q657585$D031FD94-80D0-44A9-BAFB-3B05A18E9162","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$2F5E34C5-6B05-4402-9FF6-1E0FACBDE86E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q657585$D1F9F3AE-A5E3-40F4-B321-10187C4C8E2B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d18332c0d136e13d230d0e0f2dbad96dcdac8771","datavalue":{"value":"5996003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q657585$261A6F23-73DF-4959-836F-9D4D0AC28B5D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q657585$E760C10A-0C21-466E-B3A8-C95EFBAA4981","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$E7F1996E-7478-4BD4-90F4-C37F6FB3CB00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$C5286931-D304-443B-A2A7-98C170CD3B4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$872227BB-90F5-4A87-9C65-111AEF5C701E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"31d2ddeef485fccfd3a5fe32ea329d2b65b4f1b4","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$8418FCDD-77A8-4FF8-B48B-32D0F6385643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"01712194c207617871fd4fb99ad1e9fcc6e71eb8","datavalue":{"value":{"entity-type":"item","numeric-id":15955,"id":"Q15955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$4978298B-E1D7-4A78-8287-20F2E439351E","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":"Q657585$115BF6EC-8FE5-4BFD-A292-1062FE2DB122","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a51fdc1f829b07c14d00b425beeaff90ea0aa620","datavalue":{"value":"W2025572920","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q657585$3B344165-AE79-4A9A-A6B6-4A14B265AFAC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"86187cd049bd6565ddbc4e21f37dc55f378bee76","datavalue":{"value":{"entity-type":"item","numeric-id":1250223,"id":"Q1250223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$376B0E2E-7559-47EE-87A5-7416ED4F5B2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9158c1a3f4d4ef09dee9f07229b79db0e5f37de9","datavalue":{"value":{"entity-type":"item","numeric-id":5717453,"id":"Q5717453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$BA5E4E51-4B58-4074-AA76-D35BDD3A3BC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d997660ac0bb25fe6c840c3cc2fd320fd2e234cd","datavalue":{"value":{"entity-type":"item","numeric-id":5301859,"id":"Q5301859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$FB2A0BD0-A566-477A-8F5D-1A418ACB87FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a42635e354ed5a90dff7abb6b01b6c7ff160dc","datavalue":{"value":{"entity-type":"item","numeric-id":5462949,"id":"Q5462949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$D84B7F5A-0CD5-4DB6-98AF-447E28CC91E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5369245c683380663d43367502a396b591af1be3","datavalue":{"value":{"entity-type":"item","numeric-id":5763293,"id":"Q5763293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$E2087F3E-428D-4D22-A658-CE12879494DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6302bad08c6d927e19b49fb323243aa661b18e2","datavalue":{"value":{"entity-type":"item","numeric-id":1150266,"id":"Q1150266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$E1769D9A-F432-4016-8C0B-B3D3C41AC965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c1c5cadedaa2f71bf34fb23d0208c0ef6f0d05d","datavalue":{"value":{"entity-type":"item","numeric-id":2852358,"id":"Q2852358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$E8C53A79-5209-42E7-9093-83BD7D36EA05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77c67369fd400e469f246c9f873a75c33cc3e6bc","datavalue":{"value":{"entity-type":"item","numeric-id":4946078,"id":"Q4946078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$7D4B529D-007E-4226-B313-228A6D13C7F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$3A9F1A72-539D-4ED3-82B3-E7101B7E2063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$D6305379-F649-4DC5-955C-0DD481712FFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3cb1c9b2434043bf8272ea7e59b6a15fdb08ed38","datavalue":{"value":{"entity-type":"item","numeric-id":3941595,"id":"Q3941595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$2074281D-41D0-460A-A648-F05CBD9865D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdb23be9a90cdbdbdc36878c528ab9431a368a43","datavalue":{"value":{"entity-type":"item","numeric-id":2737646,"id":"Q2737646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$1E1A7056-0BB3-45F9-85A2-3D2801A0831A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fac8018d67440c6289d41ba6a99a91f9d3e2025","datavalue":{"value":{"entity-type":"item","numeric-id":2494223,"id":"Q2494223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$045D3888-CEB3-4D4A-B089-DB834C6CB74C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55a5c491e27bbeea4d7b95894d477a28fdcc0015","datavalue":{"value":{"entity-type":"item","numeric-id":5302558,"id":"Q5302558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$B55321EE-410B-4A0D-8845-ABD1143A830D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a49cfd6942550ad4a0d31d13bbc5815a4eee0ee","datavalue":{"value":{"entity-type":"item","numeric-id":3154457,"id":"Q3154457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$F3F2638B-2BC0-444F-8640-E58522D20F8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"666c7234e6016f29d480e80a313df003fe1be0e2","datavalue":{"value":{"entity-type":"item","numeric-id":4263839,"id":"Q4263839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$03895907-928A-45D6-B7C5-0EA48D607A21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"206cdc70bbe3c338e895b7600b5aaf2ef6f7c9b7","datavalue":{"value":{"entity-type":"item","numeric-id":2852039,"id":"Q2852039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$ABA555CE-8E16-47D7-888C-D7BF00FD1515","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1613a6ff5ac7b010de5ba58e55ebd9cdec3d5273","datavalue":{"value":{"entity-type":"item","numeric-id":5765445,"id":"Q5765445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q657585$5A120DE2-006C-4CE2-930A-6C9EF8841660","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0c270e76a96806c067cd984729de332894558061","datavalue":{"value":"10.1007/S10472-011-9248-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q657585$CCF44651-75CA-466B-80FE-9EC4928E1D90","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5caf9de33d1799cb19ca4a87514a35fe4bcf1918","datavalue":{"value":{"entity-type":"item","numeric-id":704001,"id":"Q704001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed8a74eb172322cf78dcf6ca628afab79a573ad4","datavalue":{"value":{"amount":"+0.7843999862670898","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":"Q657585$C94FA17C-B750-4782-85AB-721CAA449CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d17b1eecbcdc95803b8573d7e6232291d09bb3f","datavalue":{"value":{"entity-type":"item","numeric-id":4733440,"id":"Q4733440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a38e71546ef6c7b39fc49e8378a3676d6e69d5b","datavalue":{"value":{"amount":"+0.783197283744812","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":"Q657585$E55BD1FD-49B4-47F6-A674-479C8ED388F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc268baf51e6f99f0ec7fc0e4bd70830f2cc4651","datavalue":{"value":{"entity-type":"item","numeric-id":5302560,"id":"Q5302560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89400741be6aaebbedb16c602de713a6459e2401","datavalue":{"value":{"amount":"+0.7770878672599792","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":"Q657585$3D7D1B34-7CF6-4FED-9F03-5B13E87992FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2565d9e77d9b51b905daa5bfbb63ce859f62d93b","datavalue":{"value":{"entity-type":"item","numeric-id":3345811,"id":"Q3345811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da798754f48a0a59769b7fe35d65033ccf02a270","datavalue":{"value":{"amount":"+0.7760180830955505","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":"Q657585$05A20DA0-5B26-46C7-ADA5-4F1D44EF1A30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04812e0faa39f2ad2d44990aa281e1a59afe1209","datavalue":{"value":{"entity-type":"item","numeric-id":1353941,"id":"Q1353941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b5672690f098f13f581c2c5b85b7e9e2577c1dc6","datavalue":{"value":{"amount":"+0.7728314995765686","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":"Q657585$C32767AE-B5FB-4504-AB35-583A331C15AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:657585","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:657585"}}}}}