{"entities":{"Q1309243":{"pageid":1319993,"ns":120,"title":"Item:Q1309243","lastrevid":67128069,"modified":"2026-04-12T15:28:50Z","type":"item","id":"Q1309243","labels":{"en":{"language":"en","value":"The \\(HOL\\) logic extended with quantification over type variables"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 469137"}},"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":"Q1309243$D09778A5-827C-418C-915D-5FE13C3DEC44","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f2a79a8d00a787b18f9e84d9552cf983f3930093","datavalue":{"value":{"text":"The \\(HOL\\) logic extended with quantification over type variables","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1309243$377FD105-9630-4B43-947C-01A9D08B7858","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"92d9046bca547d2e0e57612f27f751127acb9e5e","datavalue":{"value":"0785.68082","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309243$CE28D88A-67D5-4459-B7D1-DDB46725D084","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c338aef66eca0d7f93595f27eeb6b2910e13378c","datavalue":{"value":"10.1007/BF01383982","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309243$71FE87C3-66B6-4AAD-BC53-66EB8D3346B1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"237d87c04fa3d73f3e981bbff1f8797019aa6e79","datavalue":{"value":{"entity-type":"item","numeric-id":1309242,"id":"Q1309242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$889E8D00-CE8B-4677-8F1C-A33644E680D7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$9237C98F-97F3-488B-9C5D-C8C8CF9949F5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d0f506d9f4280d6b2b60ede7578329839e1e903d","datavalue":{"value":{"time":"+1994-01-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1309243$F277347C-C324-40C5-9E7D-9CC277D04234","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309243$DF4DECA5-687C-410C-B87F-00738AF2D699","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309243$25E8BC3A-A28D-4C11-80BA-3FF9832BBB09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309243$8949CA8B-B732-4863-8BB4-B806D6F14418","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3eff6d1b4699fc771281b3f30461dadda9122b41","datavalue":{"value":"469137","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309243$523C318A-A434-44A2-A28C-D8618B30B43F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309243$40ADDC69-F57C-4CD0-BEB2-1E2CF03E4675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309243$1121F3EC-80E5-4FB6-A36C-2C82A8A14F82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"485447b25ea9ae3ba0e28b66b16f57c15b7c1fe1","datavalue":{"value":"types","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309243$EA391F33-BB47-4D43-ACDB-CBA42D0DE005","rank":"normal"}],"P1463":[{"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":"Q1309243$6186C1E8-A4EC-49D8-968B-FF869BC02361","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$DBBACA1A-9164-4B60-984D-25698269669F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$9C24120F-FF68-4187-A7E5-01107AB8BF6B","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":"Q1309243$A63EFDF2-02E6-4A09-9C5A-22A06A581091","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$5C9A3667-CB45-4664-8368-6888A5E4E62A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$7E1F6803-ABF9-475A-82F6-47491F5F1015","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$4F1CE2B2-7753-48C1-A5AB-021F3F6D3C3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ee85ee408ceb2acfb30c438cac3496a36c4200","datavalue":{"value":{"entity-type":"item","numeric-id":1091379,"id":"Q1091379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$2D3D8709-D24C-45D6-BF26-4444F7A9C796","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb9e3a6772849ff9a629cad139288838375d09c","datavalue":{"value":{"entity-type":"item","numeric-id":2395467,"id":"Q2395467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309243$5C1ADE8F-C0F5-40B8-91A5-B024E015E0A0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b8ba62537928d8bef7ebe48fffd993ff15a59907","datavalue":{"value":"https://doi.org/10.1007/bf01383982","type":"string"},"datatype":"url"},"type":"statement","id":"Q1309243$E2F3BC16-6C6A-473D-8C25-9F37E72AF226","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e2102004054812fa3086811e3618410cde73daf7","datavalue":{"value":"W2997670298","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309243$AE8E75BE-BB38-4316-875B-33DD58566BAD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf735ed0349b7b682c8162ad5039bf70eddcf98c","datavalue":{"value":{"entity-type":"item","numeric-id":1945702,"id":"Q1945702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb649e044d62253ba8974951fc7597e18e67a6d9","datavalue":{"value":{"amount":"+0.9044017","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":"Q1309243$E703B250-5ECB-4E0B-9C05-04EE72F4EF0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a2a627e29f2871ae1ff628bc0545f5102ac3722","datavalue":{"value":{"entity-type":"item","numeric-id":3612441,"id":"Q3612441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44fc91ec3d18ac70857f83b3a9b4bf14eff782a6","datavalue":{"value":{"amount":"+0.90350366","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":"Q1309243$34966CB5-D286-4EF6-937D-84FDE387922F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6009f229da9cc183ad7bbbc5dd4ed923406f6b8e","datavalue":{"value":{"entity-type":"item","numeric-id":5862337,"id":"Q5862337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85bb93cf5427b87bbf3316924577d9e7427173ba","datavalue":{"value":{"amount":"+0.89401263","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":"Q1309243$ECE16DB0-54F8-4AB0-8E98-9A0B83033AE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fd5c2832aabbf4b304824c9b3020a0ed9253b4e","datavalue":{"value":{"entity-type":"item","numeric-id":4823141,"id":"Q4823141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49227699df0f579dde6c13696843d6ef50aaee86","datavalue":{"value":{"amount":"+0.891325","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":"Q1309243$E84597EC-5CC9-4D68-9D72-EB63D899DC8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0d71f2c4d6138c12ea9942329b2e7c90b943087","datavalue":{"value":{"entity-type":"item","numeric-id":5327367,"id":"Q5327367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6427fd0f4c5164caaf6c884f1951e12be8f794a7","datavalue":{"value":{"amount":"+0.8910041","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":"Q1309243$5312BA91-9DAB-42D6-ABC0-580D43C57B6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6ed608e116e5e817ab326745539b87b08cf8a7d","datavalue":{"value":{"entity-type":"item","numeric-id":3724297,"id":"Q3724297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76f00ec4380a792118d954964d7c486155f1e2cf","datavalue":{"value":{"amount":"+0.8900548","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":"Q1309243$E9C58179-9BFA-4199-95F1-72E4740EA4E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"50f559e33bdae5d6031398bd74dad7b706db362e","datavalue":{"value":{"entity-type":"item","numeric-id":4282512,"id":"Q4282512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36dfab4a7fe51bf7bdcd96a32385831d415ddc5a","datavalue":{"value":{"amount":"+0.8896885","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":"Q1309243$EB8ABD6D-FDDB-493E-856C-691F280170DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bdad91ab1fcdcd6c985f675816f55fb586ac9694","datavalue":{"value":{"entity-type":"item","numeric-id":5559531,"id":"Q5559531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94fe09a2357164e5eed8cf9bc3e1168c9802f7de","datavalue":{"value":{"amount":"+0.88864297","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":"Q1309243$93FF4212-CD12-4F04-93AD-88FF9520B33B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb62472a5c6ef87c0d6d75c2df057c2bde5a48b2","datavalue":{"value":{"entity-type":"item","numeric-id":4428704,"id":"Q4428704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28ef0bbed942cd651b88e910223c6f3f5ae70400","datavalue":{"value":{"amount":"+0.8876659","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":"Q1309243$9DAC454E-ACC2-473A-A4C7-E4BDF8EC2B72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66329513ed08c576d00231a95784464d1d411a61","datavalue":{"value":{"entity-type":"item","numeric-id":4028345,"id":"Q4028345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e30ec55c0cbf570a677023451a74ddf2d4fb00b","datavalue":{"value":{"amount":"+0.8875091","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":"Q1309243$D2BF43D8-1AF9-4637-BED6-4D34D3E30071","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The \\(HOL\\) logic extended with quantification over type variables","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_%5C(HOL%5C)_logic_extended_with_quantification_over_type_variables"}}}}}