{"entities":{"Q5176973":{"pageid":7206545,"ns":120,"title":"Item:Q5176973","lastrevid":94485569,"modified":"2026-06-05T06:56:26Z","type":"item","id":"Q5176973","labels":{"en":{"language":"en","value":"How to make ad hoc proof automation less ad hoc"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6411542"}},"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":"Q5176973$3F84DF1C-5F27-46B9-A9D5-BD0CD3C83F1B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"89f50a5124b26f056836473f753259bd2cf3cdc0","datavalue":{"value":{"text":"How to make ad hoc proof automation less ad hoc","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5176973$4B1FE2F5-D6CE-44E1-9E0C-1695F17AB85F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"91a18740b2790ccb287bbe76c0aee70051dd57a2","datavalue":{"value":"1323.68117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5176973$59E0CFE6-29AB-4B83-8DA7-53956EEF63C2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1d133ae1627583757683062b4019ea5db35e617b","datavalue":{"value":"10.1145/2034773.2034798","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5176973$6966EAC7-AB44-4553-92FC-9CA96E6BE8A1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6fe183d93c029e0aa92279cd45c5ae8bafa3a4ae","datavalue":{"value":{"entity-type":"item","numeric-id":1084851,"id":"Q1084851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$2FC73000-E554-4169-B0F9-3B6B8A3E79BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"03755d4aabc7831f3051426847269a4a588f5547","datavalue":{"value":{"entity-type":"item","numeric-id":777872,"id":"Q777872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$818C3C70-DA4F-47E1-BFDE-A67748B53E86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b248d705e0b51ec4722970eaa46ae5f39664514d","datavalue":{"value":{"entity-type":"item","numeric-id":1426867,"id":"Q1426867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$0619C591-8748-4A25-8BD9-532CF774D820","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"714a2f9cc11bbae3e9bb5cca0a961971143e413d","datavalue":{"value":{"entity-type":"item","numeric-id":1265186,"id":"Q1265186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$D33E24CA-8B4E-4BEB-9328-AEA873C47FDC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"53c2b631e99940a75af01dcb78353131f1ce5e5f","datavalue":{"value":{"entity-type":"item","numeric-id":5176956,"id":"Q5176956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$07E819B5-27CD-4067-857C-3D296EC65638","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a4f9d2095479a9188a341ba64fac456535929036","datavalue":{"value":{"time":"+2015-03-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5176973$D5BE8521-9DA8-4606-8FF5-03FE9A2AF2EC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"705a62eef1c11a2c3f545d27d9bf176a361284fd","datavalue":{"value":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.298.3332","type":"string"},"datatype":"url"},"type":"statement","id":"Q5176973$B66C08BD-B786-4E2B-8119-DE01D84EEDB0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5176973$498479B9-26ED-440B-8A2B-F1CACD4163CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5176973$DC1BAD84-8102-4629-8B79-3EEA16BE5132","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fc9699ade035546ae186325b51a67f0186c7c2ca","datavalue":{"value":"6411542","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5176973$72DAA7BE-F346-4388-979D-9D9AD63A9E11","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"49189e64e89b129f1d47958296081489c08ad374","datavalue":{"value":"canonical structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q5176973$7B38851F-F8E2-452D-AEB0-84A557C2E3DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5176973$E9FEA52A-47A2-49AA-90E4-4B8C65D9ECFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b5f13274800653d6f4f5e75ab58b6ff8315e087","datavalue":{"value":"custom proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5176973$2CFB9E1D-63CD-43DF-BAEE-F0ABD891AF63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09fd7e75771b7242416a6c218b13f354ebbba4a0","datavalue":{"value":"Hoare type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5176973$247B83DF-FA3C-4AF0-9FD2-A4A5834089C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5176973$A5AC1F93-57B5-4011-BD47-126DE00F3865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c80ecf21428f980362763aa3ec34b156b15c6fc","datavalue":{"value":"tactics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5176973$BB5E5217-9854-4EF6-B189-8612E10A3178","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff33796796e98480bd831c12f8abdaa6ed1568ba","datavalue":{"value":"type classes","type":"string"},"datatype":"string"},"type":"statement","id":"Q5176973$D41C81B7-7847-4EE9-9975-2FDB9D12CB44","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e72a4f8fb4d36497257be31382da278bd928d2e","datavalue":{"value":{"entity-type":"item","numeric-id":25436,"id":"Q25436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$A4E5A0D4-8A5C-4349-8FF0-9DE8460A28EA","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":"Q5176973$2A97AAF1-877F-424C-BC93-1EA2004D68B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$B4032B4C-ADC2-4D39-8884-ACEA3784B8F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$C407E0A1-3B80-4990-9197-A92F80DAA4C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"86fd017762a2cc84520acf70ff19531594c257aa","datavalue":{"value":{"entity-type":"item","numeric-id":33173,"id":"Q33173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5176973$F4143382-44EE-4579-AA98-4FB5706ADE16","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":"Q5176973$6D2C2B61-2889-4E3F-ADE4-9BCF900188AA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1e9fff862831c7475fa9952dfc799a41f410f26c","datavalue":{"value":"W4214826241","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5176973$6068ACDD-15CD-49F4-8375-3C2154F4F91E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b7ac36ed718b6e97928eb57ef2af05bff63f6d3","datavalue":{"value":{"entity-type":"item","numeric-id":5398327,"id":"Q5398327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f5bad60f5d71e07f84653e70422d32de406082f","datavalue":{"value":{"amount":"+1.0","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$F7828338-641E-46F9-B79B-7DD87325CB3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"448d3fdd2fd865cda8d1d7b2b7d42246a159d8f3","datavalue":{"value":{"entity-type":"item","numeric-id":831930,"id":"Q831930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a285b8bce48d31ddb524c888adb584ad2a00156","datavalue":{"value":{"amount":"+0.8047345","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$DB8C1202-6CBC-4321-8FBB-F2E16E711313","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc22a892f290f6d6ac15b5d1402ac2bb9e5071be","datavalue":{"value":{"entity-type":"item","numeric-id":2810691,"id":"Q2810691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d11a8d239d6fe26d27a55012ccbfaf6a3211109","datavalue":{"value":{"amount":"+0.7797065","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$6AECE112-BBB8-4C28-9B3B-11A5D8DBC282","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8db65f4a30f1bfae13dbc2dde40a4f8521358003","datavalue":{"value":{"entity-type":"item","numeric-id":2432769,"id":"Q2432769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c255c7f8d8255fa86c7350129b5a3e76e713d4c8","datavalue":{"value":{"amount":"+0.7785253","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$024F3EEF-7332-4DFD-9B45-8DF6D89C9E40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6706f674745437a28e826927d52883b093061b9e","datavalue":{"value":{"entity-type":"item","numeric-id":2988387,"id":"Q2988387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ca9cd6b4c5d7f7d0ba0edc5e2f1cd317da7ab3e","datavalue":{"value":{"amount":"+0.7495992","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$58E621B1-4E14-4328-A53F-96BA83EFFE8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68c709b86cf7ff4047dac00daa01e8a4e28d9c32","datavalue":{"value":{"entity-type":"item","numeric-id":4023458,"id":"Q4023458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d46555d38de472a0baa3f4ea57d1e79967cf9a2e","datavalue":{"value":{"amount":"+0.7481117","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$501CE3EA-5026-48B2-B2CF-55BF8B16A6A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7794f4628f5ef7b30a2ea8516553f1e820cc75c0","datavalue":{"value":{"entity-type":"item","numeric-id":3805958,"id":"Q3805958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec90417d387a44ec8ae5bc85da87552c4a5e09ec","datavalue":{"value":{"amount":"+0.74307","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$2D4167D6-776F-4F2D-B61C-4C60C681BB51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bedcca7522067bd4c9657d84c45f2b6bd8d3026","datavalue":{"value":{"entity-type":"item","numeric-id":1272613,"id":"Q1272613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d01e371e585cbef77c958bb11cf099a3f8febb15","datavalue":{"value":{"amount":"+0.7429195","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5176973$3FBB6D4E-8148-4E4A-8A8C-6B2C8902104D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"How to make ad hoc proof automation less ad hoc (scientific article; zbMATH DE number 6411542)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/How_to_make_ad_hoc_proof_automation_less_ad_hoc_(scientific_article;_zbMATH_DE_number_6411542)"}}}}}