{"entities":{"Q5900725":{"pageid":8007028,"ns":120,"title":"Item:Q5900725","lastrevid":50958566,"modified":"2026-01-15T22:40:45Z","type":"item","id":"Q5900725","labels":{"en":{"language":"en","value":"Proof search and proof check for equational and inductive theorems."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5695411"}},"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":"Q5900725$0FC30F0B-D022-42CD-B790-A14C60272870","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7e7c3f040a8feb248e6dc29a1def291c92088958","datavalue":{"value":{"text":"Automated Deduction \u2013 CADE-19","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5900725$9569EC84-E714-465F-87E2-381AC19F3DEB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fa02bd9af27e12bceff5cde9c61e46902937fb55","datavalue":{"value":"1278.68257","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900725$EFC869B1-DD1E-4A7E-AFE1-88DC2187305B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8a8d73ea00602924161c98d4d68a4f4ae0ee5dfe","datavalue":{"value":{"entity-type":"item","numeric-id":3553445,"id":"Q3553445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$ACDE1852-DBEE-4638-90DB-1B3BF52013F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"67de4dcf41337233b478a60d1d06381752453e30","datavalue":{"value":{"entity-type":"item","numeric-id":857912,"id":"Q857912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$17B2D14E-17C0-402C-84C9-AD1E00A8D57C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"318dcafa750fdebd097595276bc4d8a687f38a37","datavalue":{"value":{"entity-type":"item","numeric-id":271708,"id":"Q271708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$254EA024-E9F8-4CFF-9751-DDC01F409875","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"51915c997a0de468f9e9bfcf36ae19c404891d3e","datavalue":{"value":{"entity-type":"item","numeric-id":1868510,"id":"Q1868510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$D328908A-1618-4F77-8CF0-7A64DB916D2B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$C9966E70-3105-490A-8650-01B3582EE4A0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c61bb6d282cc95675f5b726985d020f8b0e6f23","datavalue":{"value":{"time":"+2010-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5900725$4A8047FF-C556-40F7-A97E-971697F30A13","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900725$D06D42D7-6AD0-48C5-A3B4-0634C0B59A77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900725$17FCD4BE-40F1-4B62-854E-6B33C3D73616","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a6ffb373e74960b52375e6a7f85a5fa4a7640539","datavalue":{"value":"5695411","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900725$468B5EEE-A235-4EF9-8F40-7EBD3EDBE43D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5900725$05E73820-D6C6-47BD-878D-314843BF60A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q5900725$AB7D1B44-DAC2-44AB-BC32-D625FF6160C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b399e80d32f01f0e5ecb7d27abf0eef31abf6cda","datavalue":{"value":"deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5900725$5BE5D89C-25D6-4D28-B751-D57B7061FDE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"90b2ed3c130c30bac7174fa9b54a06645cc1227f","datavalue":{"value":"computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5900725$36B8946D-DA5C-4825-BDB6-FA1CAC3A7B30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9168a78ecc72716f6c4bac412ea5f930139f49bf","datavalue":{"value":"rewrite rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q5900725$A0239EC8-75D4-40DB-9BE7-CCF81ABB5A3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1f66f838ab6c659c40577faeda90140c2435bc","datavalue":{"value":"proof terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q5900725$349CCDA1-C27D-4C53-B304-460D376093AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa8a6101ff90bea77f851517b5a991ddcaf7286b","datavalue":{"value":"induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5900725$C3713C02-2E2F-418D-8CBE-E69DAC3497E6","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"172e13e561e0b6f3068edccdefd44ee4b1d90adc","datavalue":{"value":{"entity-type":"item","numeric-id":14723,"id":"Q14723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$10774B0C-5BFD-41CA-B104-C09CBFB949B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$32CC39A8-D6D0-48E4-911D-56FE38DC89B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$270FCF05-1827-4286-9DB0-A6C3A867B936","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$3A5BA9FF-A88F-47DB-87D1-5F26F2561E3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af3b5ddb4818ec81bb9bea3bab4852742bff1bd5","datavalue":{"value":{"entity-type":"item","numeric-id":22101,"id":"Q22101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$91841110-FD46-404D-B49E-8553B4EB4C5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4b1f4655c4093a6763ca4d938d08d8f6020262f1","datavalue":{"value":{"entity-type":"item","numeric-id":22153,"id":"Q22153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900725$2BC37F26-9E40-4D26-800F-B61209107417","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":"Q5900725$7FBFF213-749C-43FC-9021-8B8073FDDF9A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c1c668ddb4fae172b1931ef73496e5bcbc0e7e0c","datavalue":{"value":"https://doi.org/10.1007/b11829","type":"string"},"datatype":"url"},"type":"statement","id":"Q5900725$83AD3B78-9057-4921-95B8-F13B159C7E88","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5f2de3997ca74820eaa5379240d8d8210d2079dd","datavalue":{"value":"W2483160171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900725$FA6BAC5D-DB19-460C-AA0D-536957D39F59","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"77803cf595c8808153636f8e001b2ddb16a0f0ed","datavalue":{"value":"10.1007/B11829","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900725$63123070-5560-4012-80E9-ACC2AB91E855","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7496a3c185ef40281587a6d881226db3db690d6","datavalue":{"value":{"entity-type":"item","numeric-id":1868511,"id":"Q1868511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10335b21d25c492298886d24aa22447964a131d7","datavalue":{"value":{"amount":"+0.7619538903236389","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":"Q5900725$8C1E1ADD-B4A2-4C39-8727-6FE16FBEC9C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b85b92a612525e53f1940e47c9de317d158f38a","datavalue":{"value":{"entity-type":"item","numeric-id":3608814,"id":"Q3608814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f6b848bf4d5eee60babb6993d3c83463f8464041","datavalue":{"value":{"amount":"+0.7500303983688354","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":"Q5900725$7061ABE4-1E90-4BFA-86B9-8AD53525B8A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3dc42060a3c506d7dd41e1120918b2d738a6ec64","datavalue":{"value":{"entity-type":"item","numeric-id":1601835,"id":"Q1601835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6250aa0882efd359089db8be703a095d7e60bbc1","datavalue":{"value":{"amount":"+0.7491308450698853","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":"Q5900725$EE660D19-324D-4CED-B68F-572FA215EF4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e6ac4cb02e20675307831c42232123371dc251b","datavalue":{"value":{"entity-type":"item","numeric-id":1037404,"id":"Q1037404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46a6ba211a83aef86b0b2cf47eb4df345267a140","datavalue":{"value":{"amount":"+0.7442130446434021","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":"Q5900725$F9FCA3A4-16B0-46F5-963E-C6EE70DB3C69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9d46345375cf30c0ce392ba2457e734405cc9d7","datavalue":{"value":{"entity-type":"item","numeric-id":5096184,"id":"Q5096184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd6da828f800c63f09b0054fa72c4a590c0868cd","datavalue":{"value":{"amount":"+0.7418768405914307","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":"Q5900725$0BAB5BEF-94AA-4C2C-ABEF-F09C44992452","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5900725","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5900725"}}}}}