{"entities":{"Q2881098":{"pageid":2891818,"ns":120,"title":"Item:Q2881098","lastrevid":58048479,"modified":"2026-04-03T14:39:08Z","type":"item","id":"Q2881098","labels":{"en":{"language":"en","value":"A synthesis of the procedural and declarative styles of interactive theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6021347"}},"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":"Q2881098$18B3BFCC-0C1B-4E3E-921F-49DA2AA6BFD6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f4ce7aa5a550eaf9f5e47c4efbb0a7a0cb2d45c6","datavalue":{"value":"1238.68147","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881098$28189F7F-181C-4FBC-8621-FE2B87E368BB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bf5d50c0579f3581f9a1768ce65caa6bfc42e664","datavalue":{"value":"10.2168/LMCS-8(1:30)2012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881098$957492B2-B1FC-40AA-942F-3DA2AC8AA636","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c24cc198e7b26916e61ffb256f7b2af313e3e7ee","datavalue":{"value":{"entity-type":"item","numeric-id":865657,"id":"Q865657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$BC4EDC44-D47C-4DD8-9B5C-AC1063F70D90","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$0CAE87B2-BC45-43AC-B4D4-F6CDD30A4218","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d567b51f320d6b206f1e246178a080db047a3948","datavalue":{"value":{"time":"+2012-04-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2881098$D8DAD1B0-9186-45D3-9AE1-E61E89414311","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a2fdd1bbd916f7e12c33093db63e99c47c89d40b","datavalue":{"value":"https://arxiv.org/abs/1201.3601","type":"string"},"datatype":"url"},"type":"statement","id":"Q2881098$B7CDEE30-A55F-47D8-A582-0506770C2376","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881098$73C975DE-298D-451D-9C42-D48795D41765","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881098$A174E6A6-D408-4DB2-A192-D41907719E0A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2d61e8a91f49b1cb6adc87685591fd5724cd8bde","datavalue":{"value":"6021347","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881098$DB7D535E-D879-447D-B6C5-5674D7903028","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$95FBDD4A-A29A-4361-9F97-379A2DA96B8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$9F20CEBB-762A-4FFF-BCFC-0C4EAB1668D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$2EC9EAFF-4AEC-4B4E-87EE-4DB1977A431E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc238ea6cb52c715bab39832f2cd5b4837c9294f","datavalue":{"value":"formal mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$80A3A641-85A2-4E71-B6FA-7DD3163688F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"294d237422d8f10c1ac78a363cff072c1230e8bc","datavalue":{"value":"procedural proof style","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$052CCF20-785C-4AC4-B437-06A51A6797CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39124c98f06dfe3b768e0e1841c2a5e10e5d3b5f","datavalue":{"value":"declarative proof style","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$E32AEBDA-3F3A-489A-BCC3-911034001AB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c80ecf21428f980362763aa3ec34b156b15c6fc","datavalue":{"value":"tactics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$714B431B-3246-45E5-B4F2-B019A0996023","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7541082dd79263d92182aa373330cdb16f1ad9","datavalue":{"value":"\\texttt{HOL}","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$14710502-62EF-43F9-998E-E94E281DDA9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c8099541f1cabb374567a4c1f9fb4dfc5885e5d","datavalue":{"value":"\\texttt{HOL Light}","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$3661ECC0-FA7D-4ACD-AD5E-51CF38EF2E6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0a52f2abcde2ed5d506d011173fb6a54f2d1010","datavalue":{"value":"\\texttt{Mizar}","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$7AE2FA50-5485-429A-811E-461194A2A15D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e8c8bc9aa9c27132e2597b5abd6bd0f1d721437d","datavalue":{"value":"\\texttt{miz3}","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881098$72798F91-8255-4D2D-820D-7330A3F267FA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$5AAD0B0F-DB31-492C-921B-47AD2C83038B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$0DEA70A5-DD95-4BF1-AA35-B02B5557922F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$527F21B0-2CD2-46FF-A3DB-BD729D32A021","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$B5B2E8E5-CA12-4151-9063-97CD16882DE7","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":"Q2881098$4A44B78A-049E-4C65-9C8A-7617352044C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05ea0f807e9dc1229f0a5e44480e85f8c5ae2877","datavalue":{"value":{"entity-type":"item","numeric-id":14521,"id":"Q14521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$A8F1CD2C-92D1-4970-B478-D7CB63C841BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$A36CBED6-802F-40C2-99CB-7A4E3FA10A9E","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":"Q2881098$B2483B34-20B8-4A3E-8177-3373B052EC1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"550541b08bcfd7113a03dc69a25fcd69cb35ddef","datavalue":{"value":{"entity-type":"item","numeric-id":25224,"id":"Q25224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$B3D604EA-DD8A-42ED-B96A-0C7816FA3BE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$F6D64084-9252-4A0C-A11D-B80C63C4F0FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$8E139DE4-02EA-4B2C-A099-177DD2812274","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":"Q2881098$03034E15-0B79-4266-B886-A8BE68A9FFF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$25C6E385-7205-4317-B8F6-39D373015A33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aef42c0ba3ebb76b2efad2df262c05b22e73e922","datavalue":{"value":{"entity-type":"item","numeric-id":21953,"id":"Q21953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881098$443F6CFB-5E2C-41A6-862D-89936953D076","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":"Q2881098$0A126A90-C48E-4755-9A80-B2AB1064965F","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":"Q2881098$5F7EBC80-2BDB-4CBD-8C4B-005BFE5B5241","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3e19591a8cb03f61eecbd216d3cb70dfaa12f2d5","datavalue":{"value":{"text":"A synthesis of the procedural and declarative styles of interactive theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2881098$9E4A61E6-F277-4937-AC6F-5B2DD33FD56D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b542189a171fc85ab7c4d95fcceb7c87d41da70","datavalue":{"value":{"entity-type":"item","numeric-id":4790672,"id":"Q4790672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"081f1aa0670ab67d06d2c940eaba95751603e066","datavalue":{"value":{"amount":"+0.8474562764167786","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":"Q2881098$3C26B401-4504-48C0-BE84-2145846E5977","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"60f2455c9872822fab6d8bb0ea3a402ab12360ee","datavalue":{"value":{"entity-type":"item","numeric-id":5234717,"id":"Q5234717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"081f1aa0670ab67d06d2c940eaba95751603e066","datavalue":{"value":{"amount":"+0.8474562764167786","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":"Q2881098$430EF7F3-098C-4266-B3EB-73612E9343FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"276db41e49fbbf97c9b194f4b787dd9c28797e01","datavalue":{"value":{"entity-type":"item","numeric-id":3638254,"id":"Q3638254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0813442663eda8f6c5bc6df323f578978967af4e","datavalue":{"value":{"amount":"+0.7971265912055969","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":"Q2881098$89BD7C98-C62B-46BF-B481-2CB4541F3185","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fdacfe22444d13db371f1a3adcb616ce2fa0fd12","datavalue":{"value":{"entity-type":"item","numeric-id":4484339,"id":"Q4484339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b49afdb68e61cca7610d60d0a4738021462c08ba","datavalue":{"value":{"amount":"+0.7799356579780579","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":"Q2881098$2BFD55FE-88D1-4DF5-BE77-09E2CAE0A923","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c743139fa082f66c84f8ff6b216989e8a4eab7b","datavalue":{"value":{"entity-type":"item","numeric-id":5747644,"id":"Q5747644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9a072997c10fd7366d06f75f615c2ac8da0d63c","datavalue":{"value":{"amount":"+0.7732306718826294","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":"Q2881098$B7339C3F-07B6-4E72-90EC-C454B0053770","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2881098","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2881098"}}}}}