{"entities":{"Q1819945":{"pageid":1830687,"ns":120,"title":"Item:Q1819945","lastrevid":69402441,"modified":"2026-04-13T06:45:52Z","type":"item","id":"Q1819945","labels":{"en":{"language":"en","value":"An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3995080"}},"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":"Q1819945$EF5EFFB9-C5F5-4324-BE54-BB36F6F4EE5A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4cd280eb17b685b0c905892c029a495249fe97b7","datavalue":{"value":{"text":"An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1819945$C9E683DC-B792-4D51-9B37-A38F14D441A6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"937ab54178843a7f2e96c3eaa86cad8632e65cd8","datavalue":{"value":"0614.68062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819945$D3D8E0D4-5253-4EB4-8B4D-D14048EA9651","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"87348ea07a1e710d3a5b427de71ea6bd9180a091","datavalue":{"value":"10.1007/BF00244993","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819945$3DFCD0B3-4827-4662-BC66-28214763338A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"74ab161205b2632de50aff2567915fa99648a937","datavalue":{"value":{"entity-type":"item","numeric-id":1187852,"id":"Q1187852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819945$F7C90159-072E-4EB0-9E2A-FA290B4C8989","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819945$0D5EA9DF-3054-4542-9F7C-87744A9B7B52","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1819945$EA2518FD-3E41-4C35-98C1-BE6F24CE0992","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f070da71a55195785602bf3e722dd0db760f872c","datavalue":{"value":"This paper describes the use of the Boyer-Moore theorem prover in mechanically generating a proof of Wilson's theorem: for any prime p, (p- 1)! and p-1 are congruent modulo p. The input to the theorem prover consists of a sequence of three function definitions and forty-two propositions to be proved. The proofs generated by the system are based on a library of lemmas relating to list manipulation and number theory, including Fermat's theorem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819945$FF16EA75-5484-4355-9A1D-B49A1F34DC12","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819945$7F8223B0-5D02-40F9-BB72-A6927B6D5A2E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2dd204351a4f78f61a3a371c34cc9518953a9eb3","datavalue":{"value":"3995080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819945$958C1CDB-BDBA-48E2-BF8D-F5EA17F8C3EC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d2aa687cef17cd912aad76972cec097c0540be8","datavalue":{"value":"automatic theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819945$C715E4BE-218F-4BCE-B692-3C844ACD49A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67935c9745e86097c5a009e8bb47d5846729f37a","datavalue":{"value":"Boyer-Moore theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819945$76774C0E-307D-46D3-BE61-66F846E9DAF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf9020b9cf738e3dc19adb35ae396c6478d2142c","datavalue":{"value":"number theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819945$3E4A3840-5951-422E-AEAF-8A2BF5869B23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ad64d32309503bfb4ff51d35a87b8d7c05314216","datavalue":{"value":"Wilson's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819945$043C2F3E-FE19-471B-940D-A2E2E08496C2","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819945$77C14B94-5C37-4518-B7B9-349DB28D6900","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":"Q1819945$8F56D085-113C-41FB-B8EC-83CE8C0D099C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5d7518c8654a761680343d478c4014cfa5ac2dea","datavalue":{"value":"https://doi.org/10.1007/bf00244993","type":"string"},"datatype":"url"},"type":"statement","id":"Q1819945$58E6BB18-132B-4993-9703-51315E183159","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"03f87af3fa378f2573421ed1a0de3d524930b32e","datavalue":{"value":"W2008655451","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819945$330FB7E2-501A-44C7-B84B-F3EBEFA0E702","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9ddf0154da1ac74f8cc17ad93bc59843db5d301","datavalue":{"value":{"entity-type":"item","numeric-id":1187853,"id":"Q1187853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c125ece4483dd35152468022db613561638d2c9d","datavalue":{"value":{"amount":"+0.7892331480979919","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":"Q1819945$EEC6930E-2F73-43E1-961C-725E05DB3C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbd5d69562f578d634c455a50b951c3cba745c07","datavalue":{"value":{"entity-type":"item","numeric-id":3773394,"id":"Q3773394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0b3a587890f243ebd6edbc2efc629cadd3e22c4","datavalue":{"value":{"amount":"+0.7892121076583862","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":"Q1819945$1132B09F-B2BF-4E7B-A651-EFCBEDAA93AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"98a3431f4b84ba770ea6bc555f77a5abe22d44eb","datavalue":{"value":{"entity-type":"item","numeric-id":1707601,"id":"Q1707601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f355a55d950793fbdf97c79dceb44c7fa96ef507","datavalue":{"value":{"amount":"+0.7677109241485596","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":"Q1819945$FCB95729-8F8B-4924-8A65-DE7102559F06","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":"a502e0fb99364f33c124ba00b5f2ae3b9b903208","datavalue":{"value":{"amount":"+0.7619356513023376","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":"Q1819945$D86678CC-1B86-4986-AFD0-D83C5E897D2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a06c650cf46594c2b890591bcdd84398aea42c7","datavalue":{"value":{"entity-type":"item","numeric-id":2366695,"id":"Q2366695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"02a7e6184d3a2bfe6b21000a6c4c8a066f11953a","datavalue":{"value":{"amount":"+0.7614363431930542","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":"Q1819945$79303672-5D8B-4B62-B6AB-3F5AFA2D4306","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_experiment_with_the_Boyer-Moore_theorem_prover:_A_proof_of_Wilson%27s_theorem"}}}}}