{"entities":{"Q1856145":{"pageid":1866887,"ns":120,"title":"Item:Q1856145","lastrevid":69121521,"modified":"2026-04-13T04:55:15Z","type":"item","id":"Q1856145","labels":{"en":{"language":"en","value":"Using an induction prover for verifying arithmetic circuits"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1862269"}},"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":"Q1856145$D9A0D78C-31F6-40D6-8324-3F53936313B3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"89fa7db5398801d2b07f0c0401c497ba67bf0386","datavalue":{"value":{"text":"Using an induction prover for verifying arithmetic circuits","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1856145$DF2C8A9F-CACF-42F7-B7E9-C27875F60453","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c16f312ec0c77d8141a21368b502aaadd336a728","datavalue":{"value":"1059.68527","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856145$01657473-C8AA-4156-A1E9-BE61D8D2CA19","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e3039db9ee74c8eaadf696982a16b57892d18cb6","datavalue":{"value":"10.1007/PL00010808","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856145$BD655E6E-64F1-4430-AA4C-78E35DBBA329","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a60a38320311da18eda10821922742954865726","datavalue":{"value":{"entity-type":"item","numeric-id":394492,"id":"Q394492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856145$3CAAA3D4-8098-4A32-9474-5739B750D8D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc3c07fe67798adad374606ca167de6f17564996","datavalue":{"value":{"entity-type":"item","numeric-id":1856144,"id":"Q1856144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856145$45605A2B-5805-4407-8B3E-CBB45CBDE429","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e1846ce75b2b308fd593b292d943abd351ca6751","datavalue":{"value":{"entity-type":"item","numeric-id":225063,"id":"Q225063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856145$4BF8EEEF-B713-4AB3-8E22-EE71075A84DC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"51fa866876a61ae2435740199de51e5bb1a31ee7","datavalue":{"value":{"time":"+2000-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":"Q1856145$4C663810-93DE-439F-8EF8-907F33C6547D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8d8a22ace48964288ca1ed080fca5299ff532395","datavalue":{"value":"68M15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856145$AD8FFCE0-A3FC-489A-BD31-F943E030B02B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856145$F15FD965-DE4B-43E2-A87E-5F588A1C6749","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9e4be5ab57d9c652ab8343b63de66b7a1ebaee2f","datavalue":{"value":"1862269","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856145$9C5FF7AC-7042-4A92-87D5-A56712AC5C8C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856145$3BAAB3C6-C870-4379-8A9E-1BA8611F15E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac52900f9c775a1c2e9b77521a060cf4681ca7f4","datavalue":{"value":"hardware verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856145$01FE339C-4457-4490-A8BF-53C6E9FF5B41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"476e70cc5d552d5cdc76575cc73d40a8bfb4b86e","datavalue":{"value":"rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856145$C47B4133-5D97-4276-8C91-7DAB52D041C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"916f2a5439f7e4b36d4fe8bc533c45ce2dc6fc9f","datavalue":{"value":"arithmetic circuits","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856145$5C754CA4-B9C0-45ED-AB60-C3639CE6854D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856145$5C8759F1-08E3-4A69-A06F-2026D62C88B8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3f1ebf2accc5d6c6b3c7a81ee7493fd53a6bf250","datavalue":{"value":{"entity-type":"item","numeric-id":40618,"id":"Q40618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856145$7BF9B9C9-5146-430B-9278-8AAEC08A074A","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":"Q1856145$2C4243D9-2AF1-49D0-87EA-7450AF5C624B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"048c8f0371cc123ef275991e881bb7050fb753fd","datavalue":{"value":"https://doi.org/10.1007/pl00010808","type":"string"},"datatype":"url"},"type":"statement","id":"Q1856145$968EF09C-3C26-4140-9421-8E65B68F3E59","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"95cb6378fc238e40082cb55adb71fc582b44064c","datavalue":{"value":"W2091905929","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856145$3EC227C8-1534-4A0C-9511-B7CBC144F9AD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"714e15e5a2ba4fff06e9121fed38d3236869a4fd","datavalue":{"value":{"entity-type":"item","numeric-id":1267035,"id":"Q1267035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da44aacd4d53cc0ceb10447b93fd14ffba61e6c4","datavalue":{"value":{"amount":"+0.88270134","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$8AEF789D-5AF9-4724-814F-5BED4168E53C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45a5dc7e2a40afbea7ab60e8677820b20926ba87","datavalue":{"value":{"entity-type":"item","numeric-id":1915133,"id":"Q1915133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"306693ff56129c96411ecd7687da25ce3c81f7ee","datavalue":{"value":{"amount":"+0.87828517","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$249976C7-D40F-48D8-A23F-686F39028943","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aba5e2dcc44965bf730a7b641892b0f206ac96bb","datavalue":{"value":{"entity-type":"item","numeric-id":5108030,"id":"Q5108030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dc8ef5eec148a6dd36e77c5fd64f8f8f4aec7c5","datavalue":{"value":{"amount":"+0.87645984","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$8E0A6BEE-BFA7-4E1D-B131-D82B7B6EC7E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be43729fe539971fdf1aa681af41ce8d0f28afde","datavalue":{"value":{"entity-type":"item","numeric-id":2852038,"id":"Q2852038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bf1bdf7152eebbbad77d8bda0e6e739e42304fc","datavalue":{"value":{"amount":"+0.8700855","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$225516B2-A499-4702-AA9D-796C65C07E1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f225124d15a7a6aa53392ac079722a1eb252bdfa","datavalue":{"value":{"entity-type":"item","numeric-id":3345810,"id":"Q3345810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"706c15f3176806663ff5a363b6865b60ae145239","datavalue":{"value":{"amount":"+0.86655843","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$4ABB5600-5F5F-4580-969D-D01332FF4A95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9c23c68c5259250489a992c535acc7120127fcd","datavalue":{"value":{"amount":"+0.8662902","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$B3C3FC34-FF03-416F-945F-F345520088E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aec02a95d2ddd1c5c73d7dfb4ad2ff29b6d075f8","datavalue":{"value":{"entity-type":"item","numeric-id":6487296,"id":"Q6487296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25679c7529640e514cbd0b95bc6da86396f9896b","datavalue":{"value":{"amount":"+0.86596745","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$2384F580-21AA-479C-A583-E3617C0666BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d7da2d8bb240c114f0886df7c3e68f858256d058","datavalue":{"value":{"entity-type":"item","numeric-id":945055,"id":"Q945055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a2eca2cadc5eacbcbea5ea193ad15c160a3791a","datavalue":{"value":{"amount":"+0.8650975","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856145$83D327ED-5308-4DEB-9B36-8BEC1D115DD5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using an induction prover for verifying arithmetic circuits","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Using_an_induction_prover_for_verifying_arithmetic_circuits"}}}}}