{"entities":{"Q744079":{"pageid":745928,"ns":120,"title":"Item:Q744079","lastrevid":64047918,"modified":"2026-04-11T17:17:28Z","type":"item","id":"Q744079","labels":{"en":{"language":"en","value":"A systematic methodology for automated theorem finding"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6351421"}},"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":"Q744079$97BE3D8D-7E79-4A54-823D-6116D41ABCBA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c6467af68cad2e2ad2c21702b0d5a4767c4bc916","datavalue":{"value":{"text":"A systematic methodology for automated theorem finding","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q744079$86895B43-948C-46C8-86D8-3535A7AD765E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"88afcd409886fcfd02e12afa2fddfb28ba13aa45","datavalue":{"value":"1360.68749","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$4490140C-B2D4-4925-B587-386B61D0B4AA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6dd390fe29df8912b04d7f9fbbc9b55e428c39ff","datavalue":{"value":{"entity-type":"item","numeric-id":744076,"id":"Q744076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$B5B75C99-9883-4D9D-BB38-16D62AD059C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"885600df7f84b3469ef4d6ff7f0c0f0b7f0f1625","datavalue":{"value":{"entity-type":"item","numeric-id":744077,"id":"Q744077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$48B34CAE-11F1-4BF0-9CE0-1D8CB2F771C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"29583797441d21324f80fd397bb4d819a7ed2765","datavalue":{"value":{"entity-type":"item","numeric-id":744078,"id":"Q744078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$F9294173-99AD-4835-B998-EEFAEFC829C8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$228B1770-E8B5-4C4B-BAB5-FA13707CE4B0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a2b61fc3e1fd77a44c6756723ec563e89b4b6f26","datavalue":{"value":{"time":"+2014-10-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q744079$50AFFB2F-F1CE-433F-B7D8-EBE0FDE72D73","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$2DB0D198-BB36-44EF-A0C5-79E4211A69E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$90AA9D76-68F2-4E98-ADA8-BAEBBFFD7179","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$F447DCD2-1543-4E12-8ECC-AE0CD166E71D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$37C57CC1-74F4-4D3D-9C56-4BA91AF3EF6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$7FD03003-B095-42D8-B220-86B36DB3933A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"696016a4bf7615b60a427530d8c76ac49d60d1af","datavalue":{"value":"6351421","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$C7094B4B-047E-4CA6-A491-01903F4A5D94","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff9d1ccdc8ec6fb39fbce9ca87278a57e1a2802c","datavalue":{"value":"automated theorem finding","type":"string"},"datatype":"string"},"type":"statement","id":"Q744079$B5F2B3D6-8CD3-4B56-A22C-176D14EE4EDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"37e7a9cfd736f27ab7d00b94ead2e7b116879897","datavalue":{"value":"forward deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q744079$B201E651-CFF1-45B5-9CB4-BA51FE8ADD4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa097e1c677d0530b4b31b21a359b3b8a005125a","datavalue":{"value":"strong relevant logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q744079$90BFECB2-C077-4A8C-8D07-4A1A445C753F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e0a4b78e77b3c229c2bfe117e6414e0a8b802a2","datavalue":{"value":"NBG set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q744079$48459804-C531-47E4-9420-84A5E21A4B70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q744079$DC5A568C-1FCF-4CC6-B839-E28457EB044A","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":"Q744079$8A28C0FB-9318-41FB-850F-034587F1A07E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2d572f63f4fc78b1c8a984b92e7fc3d8b11bf4e8","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2014.06.028","type":"string"},"datatype":"url"},"type":"statement","id":"Q744079$749246E5-19A6-4EA2-A28A-BCF299476809","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ae7dbe9fd6399d0b846f9d7a6cbd6220f17f9743","datavalue":{"value":"W2000227239","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$B53DD5A8-D5DB-406B-9A2C-A0A0A1055C61","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec09860f6f4856a0bfa1fcbed713df420a357696","datavalue":{"value":{"entity-type":"item","numeric-id":4085699,"id":"Q4085699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$B21CD2A9-321F-4E72-AA6B-4CC0605D2F3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcad1b51622bd87c59556af8c797422562d18a92","datavalue":{"value":{"entity-type":"item","numeric-id":4297115,"id":"Q4297115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$8B61016C-AAFF-472B-8919-B4949DB420FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8e92ba9e528c78f1e1897eb9cbc70ea712f77dc","datavalue":{"value":{"entity-type":"item","numeric-id":4524837,"id":"Q4524837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$D338BED8-5CA8-4AED-B703-ABEEFB59A4EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ba4f5628b9493b3dc4e9b69bc068cb07ae68c2f","datavalue":{"value":{"entity-type":"item","numeric-id":4530231,"id":"Q4530231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$3F5329F4-21C7-45E2-8682-8320EA15437A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"460a35cdceca2047ff898269da0e47118625274c","datavalue":{"value":{"entity-type":"item","numeric-id":4925285,"id":"Q4925285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$CE5DA960-4D25-4E0F-B214-0BE0695850AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"847e3dcf8d17a4bf2ebc16dc465d8fb6ca2c9cf1","datavalue":{"value":{"entity-type":"item","numeric-id":4032144,"id":"Q4032144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$99E0AA9F-67CF-4B59-A558-F78900AC6565","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0620e875ace4454552471ddc26f3c19b333694a","datavalue":{"value":{"entity-type":"item","numeric-id":3994754,"id":"Q3994754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$C2741DED-CA1D-4A73-B7A7-4E43B0456941","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e276acc900bde0886719e56761a9796d27811b3","datavalue":{"value":{"entity-type":"item","numeric-id":1312164,"id":"Q1312164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q744079$AF1ACF2F-4D29-4AF3-8769-4361E89B9E32","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1a1bfd3bac7d49f832ee3c97dc5e6603d1254dbc","datavalue":{"value":"10.1016/J.TCS.2014.06.028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q744079$516F5A9C-7E5B-47E7-99E5-D2B171E848DC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb5467682780608a828507178f74fe823cf144db","datavalue":{"value":{"entity-type":"item","numeric-id":4925285,"id":"Q4925285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"213943878f2492493070f201d127fc138d9765e2","datavalue":{"value":{"amount":"+0.8966965675354004","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":"Q744079$93B9771F-C264-4A61-A2BB-46EB85DF0B8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c43d51778a5135618f05dd3b1850debad03e350","datavalue":{"value":{"entity-type":"item","numeric-id":1312164,"id":"Q1312164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4f2075f9001e54dc6e4430af4eb75434ecc9583","datavalue":{"value":{"amount":"+0.7841817140579224","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":"Q744079$6A28A705-8E2A-470F-A45F-FF9FE4A4D4F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8aea7919ebb0448a4cc56ca227584941c5cda3d4","datavalue":{"value":{"entity-type":"item","numeric-id":4721670,"id":"Q4721670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"330cffdf655d404c033b81239f8a2ec98d1e7dac","datavalue":{"value":{"amount":"+0.7352861166000366","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":"Q744079$CF9AB942-6291-4805-B6CD-26F78CACA29F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36a4004bec8c4bf76605ffb8af1d4dfe2b0301b8","datavalue":{"value":{"entity-type":"item","numeric-id":3352532,"id":"Q3352532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"570fd63b79cc34b689de15958c3fd489df0bbfe0","datavalue":{"value":{"amount":"+0.7221821546554565","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":"Q744079$8F382727-39FE-44F1-9AC3-2AE207624700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27c115c87800ff78afacf69737fff282691b60e0","datavalue":{"value":{"entity-type":"item","numeric-id":5951529,"id":"Q5951529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42505e169d89e7271a808d3f44605179b8231a4c","datavalue":{"value":{"amount":"+0.7194242477416992","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":"Q744079$6F0C8D07-9DC6-4310-BFAC-8E454002855D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A systematic methodology for automated theorem finding","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_systematic_methodology_for_automated_theorem_finding"}}}}}