{"entities":{"Q6869927":{"pageid":20716153,"ns":120,"title":"Item:Q6869927","lastrevid":84234161,"modified":"2026-05-14T00:23:18Z","type":"item","id":"Q6869927","labels":{"en":{"language":"en","value":"Exploiting instantiations from paramodulation proofs in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8149371"}},"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":"Q6869927$9D0C3C68-F4FD-49AA-937F-C39222B574F4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7731a46958db865e927fdd8e448e5f4236f82aea","datavalue":{"value":{"text":"Exploiting instantiations from paramodulation proofs in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6869927$DE5EC3EA-6B0D-4DC9-BC89-D293B46B845E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ce7764c533bbfc2b6ae9c34c2dcbfdf7e11fb887","datavalue":{"value":"10.1007/978-3-031-99984-0_30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869927$994C41A3-B3D8-4781-9DB1-11AC8476413E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"04eac7ea3a8edcbf63c60866b07b49f57a6507c5","datavalue":{"value":{"entity-type":"item","numeric-id":6869926,"id":"Q6869926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$9F4A125C-9F70-4FAE-93EA-135012A57B71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"42c29c686dffd678d9f155b05a4a1aa93e85953c","datavalue":{"value":{"entity-type":"item","numeric-id":287335,"id":"Q287335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$05C3C2F2-F294-4F0D-9EF9-BDD0F30B78FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$4A8D849C-EA6B-430C-9673-4486CED3CB45","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bd0535754d1571e407a6ce2636467dab5aaebc85","datavalue":{"value":{"time":"+2026-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6869927$2E112E47-6394-4496-929A-3DD66DAFF006","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869927$79633BB0-2104-4BA1-8A3D-EF4200FA8D84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869927$A6235D59-86C7-4230-99DB-5CBDA2FC1FDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869927$D4400742-FB85-494A-82D9-D396C24BFE86","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7341a7dedb6db55776f9dbdce96795ebd8b7d34a","datavalue":{"value":"8149371","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869927$27C82AA6-A47E-419D-9780-74BC0662134F","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$896092CC-4BAB-43E9-937F-ACE7456CFA9B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9af3f5d3f9a756b613e3b9d0b340c029a1c07de6","datavalue":{"value":"instantiations","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869927$D73DD473-BEC1-4F83-BFE1-060C242A31AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869927$39B4AACE-A757-4242-BB6B-45553B3E8789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869927$2443DD11-2CC7-4559-B4FF-E7F2E6BE4133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bbb007fa331a260b53a971b725dcae4761f63fe","datavalue":{"value":"sledgehammer","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869927$22208025-AA61-4E8B-8E87-21FAA74A721E","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":"Q6869927$711720F5-5F43-4D2D-B1E2-1E61260CF29D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"24e4d5d206133d3398c50fe5451aaece0e817a40","datavalue":{"value":{"entity-type":"item","numeric-id":6488549,"id":"Q6488549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$97BEFC0E-3525-4F15-8CB7-D56F741C8105","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67737023899dd2252d79885f477a3601bda6d265","datavalue":{"value":{"entity-type":"item","numeric-id":6114261,"id":"Q6114261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$9A2CB30B-D45A-4219-B06F-1F0C9CFB82E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aff27fba797d9b89f87ffb78f342cbfce639e6e7","datavalue":{"value":{"entity-type":"item","numeric-id":7034876,"id":"Q7034876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$B224E0A7-9B9E-4156-9959-99FB3C142621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"961e583e188fc7cff1699f17f5a1576a96a31fd3","datavalue":{"value":{"entity-type":"item","numeric-id":287340,"id":"Q287340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$3383BCDD-4112-48C9-B221-DB2B130A35F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1c6990245e88cf35ce6df13fb7eecfc9e28e060","datavalue":{"value":{"entity-type":"item","numeric-id":2974796,"id":"Q2974796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$AB5286C1-103C-4C24-8E62-B7DD2E08C26D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9ced8d6f2a9df1ee71786851c7533b59c2dba2f","datavalue":{"value":{"entity-type":"item","numeric-id":331617,"id":"Q331617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$2E0A87A6-CED1-4F2A-B06E-F02C3D1A5B1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73bc73e3351b113a1680b6365fb1851ae1d25213","datavalue":{"value":{"entity-type":"item","numeric-id":3453102,"id":"Q3453102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$2DA0968D-A200-44A9-A407-40360C97096C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b19149185e72c842c12321303888117be6b4dec","datavalue":{"value":{"entity-type":"item","numeric-id":2914754,"id":"Q2914754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$74320CD4-738D-4FB8-A9BB-759B0585C27B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e553c29e7f65e2e114458e6c7f3b8557e6ca7633","datavalue":{"value":{"entity-type":"item","numeric-id":6629514,"id":"Q6629514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$D739EAC1-7FF0-4D4C-A487-8DA92DE91A08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$020877F8-E7FC-47CF-B3CB-43F64C9FBAFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00230673e703c339b2d770b71ef179a8241cadd5","datavalue":{"value":{"entity-type":"item","numeric-id":2270573,"id":"Q2270573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$136E5D2D-652B-4CDF-86E3-353142496038","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cdef4114ad058efe7edabe8fdd17733b47122ce2","datavalue":{"value":{"entity-type":"item","numeric-id":1701039,"id":"Q1701039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$3A255AED-2384-49CB-A449-31A912FB50BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bac46cadd391b69a8eb2eb17270bc333130444c","datavalue":{"value":{"entity-type":"item","numeric-id":6572540,"id":"Q6572540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$27EA8DE0-2447-4F6D-8E0D-6B69820FC7AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68bd3c479b0afc38fc2b3684aaa9294549d85a83","datavalue":{"value":{"entity-type":"item","numeric-id":2817928,"id":"Q2817928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$6F9B321F-E67B-436C-8FB5-409D09ABCBF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f38c339bbd571c9f13a1b3052c0abde7b640b4a","datavalue":{"value":{"entity-type":"item","numeric-id":2471742,"id":"Q2471742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$9BD64920-5FFC-448C-B30B-1020961C38D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"741b1c2a1697c669d1b3bbdff87dd79f9f007366","datavalue":{"value":{"entity-type":"item","numeric-id":1006731,"id":"Q1006731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$A83256B1-0378-4DEA-AD8D-122439DE2990","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"171f2f23484cc563361b9a949250d7cf0cf0889e","datavalue":{"value":{"entity-type":"item","numeric-id":2479551,"id":"Q2479551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$A17EF289-EC00-4F86-84FE-AEBEE3C8E171","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5809a6684c365442525c649f10f3cfd46627fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1825045,"id":"Q1825045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$D14EB91B-34C2-4B9A-82F6-BFEC0E27D562","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$EDC382A9-E639-4C3A-A6F5-F5F64F4F44AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017089f1b8820cff138bb4305c5e5fd1db1ba3c2","datavalue":{"value":{"entity-type":"item","numeric-id":4850163,"id":"Q4850163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$5289AE9E-E45E-4F77-B04C-EF0FB4853768","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$5616F383-3D94-4EA3-ABDA-A9EE031C3EE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42ba0d7a787c3ddf27f1ee78a59c4dec37184a75","datavalue":{"value":{"entity-type":"item","numeric-id":4520767,"id":"Q4520767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$58687383-A8A8-4D5D-9B7B-ED4AAED8D890","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"716d170b6d9b095492bf0c2b742ee0dbade5bbe0","datavalue":{"value":{"entity-type":"item","numeric-id":3523178,"id":"Q3523178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$4F1BC9EF-79D3-414C-BA07-3651F9FEEC0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a12611ad8426de2a5be4ebcaf4b8bcaa4857ba3d","datavalue":{"value":{"entity-type":"item","numeric-id":2108191,"id":"Q2108191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$5205DD46-267C-4271-B77E-1AD81ABA458B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad1bdd6abc4d3cf5dea2b7602404acd1281c9b7d","datavalue":{"value":{"entity-type":"item","numeric-id":1799072,"id":"Q1799072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$A4B0DC88-A45D-49DD-8891-DFC4D80F86D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8470718175ec6109a436628221c5cffb3ba70aa9","datavalue":{"value":{"entity-type":"item","numeric-id":4167525,"id":"Q4167525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$E5A82292-A378-4B20-8721-96335F18F227","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59d69e7c781c6370212654a029921d34ee26dd92","datavalue":{"value":{"entity-type":"item","numeric-id":5918403,"id":"Q5918403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$3B50FF01-B0E3-4A80-A8BB-A1941B8DA67E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9149c5c2f19af238fd2b9656e997c2c32d9eb5b0","datavalue":{"value":{"entity-type":"item","numeric-id":6536126,"id":"Q6536126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869927$7E617F12-D6B7-421D-9B30-ECA4DEBCD609","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Exploiting instantiations from paramodulation proofs in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Exploiting_instantiations_from_paramodulation_proofs_in_Isabelle/HOL"}}}}}