{"entities":{"Q1798971":{"pageid":1809713,"ns":120,"title":"Item:Q1798971","lastrevid":57564804,"modified":"2026-03-31T10:26:49Z","type":"item","id":"Q1798971","labels":{"en":{"language":"en","value":"Goal-oriented conjecturing for Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6957971"}},"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":"Q1798971$D0772734-A0F0-4FB9-BE31-256C8B953662","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"05e4b709a0bedc65505c24962157c38f29226ee7","datavalue":{"value":{"text":"Goal-oriented conjecturing for Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1798971$6F00419B-4C8B-49EC-8701-EE215B250C99","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5dcfae58c50b61a3972e27dc3e9702f086f342c9","datavalue":{"value":"1417.68190","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798971$24E937ED-40FB-4436-9DE2-9AF995EBF6EC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4efe2e75ab03769cc15522d27f24d6a8cb8bd24b","datavalue":{"value":"10.1007/978-3-319-96812-4_19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798971$719ABD22-F3B8-4248-8F15-17BA647AD231","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bad250d2383a6addb9f20421ad8f0febdd8925ab","datavalue":{"value":{"entity-type":"item","numeric-id":1798970,"id":"Q1798970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798971$BC5B2C87-5D73-4D7A-95B5-E0BD106562C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b4e8b8854a2f5f1838328c162624d112c179ee43","datavalue":{"value":{"entity-type":"item","numeric-id":1791185,"id":"Q1791185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798971$CA54D691-3CB3-4ADE-A378-3FE0F68E3F6E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1798971$3545AE9C-7316-4730-8B00-B10CFA627076","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6383ae393082447f41809f79033389851e2d330b","datavalue":{"value":"https://arxiv.org/abs/1806.04774","type":"string"},"datatype":"url"},"type":"statement","id":"Q1798971$6CF57935-B358-4E27-8967-740C117C2548","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798971$254D59A0-4B5D-443E-A642-FBD1185326F7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"49fbc0e4f5372c32c56763083b018bdfa9d5cf8c","datavalue":{"value":"6957971","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798971$BDC2DA3A-3759-4EF0-970A-44DD80F741DB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798971$9D9FA9D3-F82E-4503-A2E7-2EB9E9680BE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798971$42FE141A-FE24-4C67-BC08-AC4281B38CF1","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":"Q1798971$72017187-BA47-4D34-BA92-B1D609F14E4B","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":"Q1798971$2B191D31-B927-4BC8-B902-C3BF56608851","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"922490ecc6bfc8663f65c46c4f8b5eab7b9f80dc","datavalue":{"value":"W2808288494","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798971$A3BD6D27-733E-444F-9B8C-6ABA308ED6A3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1aac3c3e28f3c5c8a5eba2ddfcb1c23067c2156","datavalue":{"value":{"entity-type":"item","numeric-id":2405272,"id":"Q2405272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42122343b15b29893219f6d2654dad11651d4402","datavalue":{"value":{"amount":"+0.7640571594238281","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":"Q1798971$F927D4BD-50AC-4867-999E-E2D7ECDDC60A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f94645fe7f1525963701159b1c6851e22f8eef0","datavalue":{"value":{"entity-type":"item","numeric-id":287340,"id":"Q287340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fef113254827096dc79b4ef02a512a5f3e27cd25","datavalue":{"value":{"amount":"+0.7597380876541138","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":"Q1798971$B8DCDBB0-3875-4849-97FE-D40DFF7E37F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38394b4e8d3a3502630a463829cd1f4840ac5524","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dbc1467e831b5ade7c4476a298d0e12aa22a03d","datavalue":{"value":{"amount":"+0.7438869476318359","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":"Q1798971$E5D6C64D-41D3-43F8-9E58-7CFF0DBC3CD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2581c12a75a0c9d896500c637ad68fa005c15f39","datavalue":{"value":{"entity-type":"item","numeric-id":438543,"id":"Q438543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7adfe4812822b35e53ba9205c3bf35b840f2976","datavalue":{"value":{"amount":"+0.7363431453704834","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":"Q1798971$EE97CBF4-2FCF-4432-B4CA-2E1F0BA9F08C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e2ce9d05c86c088573e2213f25dbf60f15f642e","datavalue":{"value":{"entity-type":"item","numeric-id":4524774,"id":"Q4524774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aff89b560779cf5783b16ddbf02a0e20350d52b3","datavalue":{"value":{"amount":"+0.715164303779602","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":"Q1798971$4062735D-75CB-476B-BEC2-AD9F8028498A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1798971","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1798971"}}}}}