{"entities":{"Q1961912":{"pageid":1972654,"ns":120,"title":"Item:Q1961912","lastrevid":47436694,"modified":"2026-01-01T18:13:54Z","type":"item","id":"Q1961912","labels":{"en":{"language":"en","value":"Special issue: Formal proof"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1394787"}},"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":"Q1961912$B775219D-707F-49E6-A0F9-502CC1608A2C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fc5edac7420ef00039b71b51bda60104e6d6bedc","datavalue":{"value":{"text":"Special issue: Formal proof","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1961912$AF0071D2-0C31-43C5-98ED-951361001EF6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7197bcaf63e9b8ca9f961d0e600cf1b3df4deab6","datavalue":{"value":"0937.00019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961912$BDB58C17-E050-480C-B098-C1C31817C863","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b8e2e3c5f0163d6451826c9f21f6038a89dae0d5","datavalue":{"value":"10.1023/A:1017202010519","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961912$BDE765C0-727B-4275-9371-28E727961CF9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961912$1F67E937-5FAA-4672-BABB-50CBBE69BCD7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8fc142a22f1f6784530e2dfe6b860e6fbdb5637","datavalue":{"value":{"time":"+2000-05-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":"Q1961912$9523827B-C7F0-4673-8237-908B64FB213B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6e3b0f0bfd2cab1df575dcf7b14ca34889759aac","datavalue":{"value":"This special issue is devoted to papers describing the implementation of a significant proof or theory within a theorem prover. Each contribution consists of two parts: (1) the paper published in this issue, which outlines definitions, proofs, formalization techniques, and so forth in informal mathematical language and (2) the code of the implementation, which is available electronically via the Kluwer Academic Publisher's Web site at \\url{http://www.kluweronline.com/issn/0168-7433}. Further references are provided within each individual paper.    The articles of this volume will be reviewed individually.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$590B040F-346F-44FA-A096-DE5AD578BC8F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"342a6161f41187e2c595daa41b09cee10ab1ace9","datavalue":{"value":"00B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961912$F375821A-B463-4708-8D8A-59A0BF688EAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961912$2FC5B7AB-438F-4C19-83AB-B70686EB613E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c75ae986d2038bf3ba1c8245d5dd6bee62bcbde4","datavalue":{"value":"1394787","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961912$BEF6E83A-248C-4FB9-AE75-F4AB07B6902E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f55e3d8717e0787e68faec0af0e711b23942cd","datavalue":{"value":"Formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$323C6950-D1A5-4FD1-8291-F567088844F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"30079201549958701bc79bc36ae8a8054f2abdac","datavalue":{"value":"Special issue","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$9C58EF34-BF36-46F8-89A2-53AB86561270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$CD616B3E-0FF1-4D11-80CF-32F0FF88B963","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5343ecd15a8e87cb138c7d9e4c8f0d52a5afdb65","datavalue":{"value":"HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$84AD5883-81F6-4E43-AEB9-36B5B9474EF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$D8B1AFC0-189D-4820-9E86-AE9F63361465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"755c433ee02ea45cd0de7e5b9b28b76f4908d4ed","datavalue":{"value":"LEGO","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$6052F005-0947-44B9-8A3D-4A20398EE586","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"571c0e1fb7a78a4a545c4f12cd6536c1efe33bd7","datavalue":{"value":"Mizar","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$C5DD8C8E-0664-4FFE-824C-3EE999655993","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3cb6d27fde1e3214c7492516628c363d07c12966","datavalue":{"value":"NQTHM","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961912$15E580B8-9798-4DBD-BBFA-58AF6B51A617","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961912$9F85D66E-5D56-452F-B6E9-F9471E569C4F","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":"Q1961912$1D838101-EFC8-4797-B95A-6F0DFF4C450E","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":"Q1961912$B9BBCB31-4B48-47A6-8A8D-61BE453F4CCC","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":"Q1961912$D1C69B41-85AD-46D8-9043-096BBA89410B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961912$F841F33F-9DBB-4555-8707-00C5BB13126B","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":"Q1961912$A57A13B3-1E80-4123-AED9-55CBDA17A778","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c32f2cbb8a453222b98cdf0e974734e0b4ea4a11","datavalue":{"value":{"entity-type":"item","numeric-id":5094469,"id":"Q5094469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"037b94262abbb28a33a306f56774d69c11f09b03","datavalue":{"value":{"amount":"+0.804728090763092","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":"Q1961912$478F7750-8F02-4250-A72F-E472962CF902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b5cd105b44770aa835c9cbc85b4fcf5656f16d0","datavalue":{"value":{"entity-type":"item","numeric-id":5894305,"id":"Q5894305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a38a13cfebbb76ad1cda67ae5a43cfe4bba737e","datavalue":{"value":{"amount":"+0.794797420501709","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":"Q1961912$3290CF56-CF1A-433C-B8DC-CC9F7F9D8DC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc268baf51e6f99f0ec7fc0e4bd70830f2cc4651","datavalue":{"value":{"entity-type":"item","numeric-id":5302560,"id":"Q5302560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e48f36d18cd9a59de1614242cd79e0a88be0119","datavalue":{"value":{"amount":"+0.7610155344009399","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":"Q1961912$9026A715-658A-403B-9864-43013B97B27F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"595f6616d7f7c7bdbfd5649089c6877995bc6cce","datavalue":{"value":{"entity-type":"item","numeric-id":2018656,"id":"Q2018656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d910846f60621616c32f5dccf5b60b9c8a1d261","datavalue":{"value":{"amount":"+0.7432258725166321","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":"Q1961912$D21E5A63-FF32-407A-80B8-4EBA9674BF3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5caf9de33d1799cb19ca4a87514a35fe4bcf1918","datavalue":{"value":{"entity-type":"item","numeric-id":704001,"id":"Q704001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7b5a65314bc12ba77bb03842605376418d334f2","datavalue":{"value":{"amount":"+0.7424089312553406","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":"Q1961912$987F0832-A8B7-4337-94A4-F8BE87C46748","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1961912","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1961912"}}}}}