{"entities":{"Q4276174":{"pageid":6305775,"ns":120,"title":"Item:Q4276174","lastrevid":89307023,"modified":"2026-06-04T16:56:08Z","type":"item","id":"Q4276174","labels":{"en":{"language":"en","value":"A Complete Proof Synthesis Method for the Cube of Type Systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 488295"}},"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":"Q4276174$A38A28AA-2A12-40A5-B49E-632BDF0018C6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"45e9632316b536313ebbaf3368b154f065140cea","datavalue":{"value":{"text":"A Complete Proof Synthesis Method for the Cube of Type Systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4276174$CE806DB1-505B-4059-BE32-D1800B56A6F1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"07808f98c37f2309da1b18f7ba40a79f41370bab","datavalue":{"value":"0789.68123","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4276174$F9F5F22E-5E56-46D6-9935-DE19851F3933","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f681530f1e601559ae451198ac16d4e80569d32e","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4276174$1D0974F5-F5CD-4300-9B55-926B024B3E65","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"27ae8e0ebd05772ccdad25ddba931e713bd9a4bf","datavalue":{"value":{"time":"+1994-06-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4276174$8FB45967-0CF3-4A7D-B4DD-D959FC1BA80A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4276174$181B88C7-69E6-45E8-9EF4-7D92B175B6CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4276174$7F82E5A5-F02B-4110-9478-50D73AEC1327","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"42c4925734508bfe133e9b57107a4c7d14e0a7ee","datavalue":{"value":"488295","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4276174$AFD503DC-2B21-4856-A8D5-E96D0285768F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4276174$D27481EB-2290-4E94-BFC3-91563635014E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9072e4a6d9dafd8c8ec2e3f84628a32b8a5ba17c","datavalue":{"value":"proof synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q4276174$943ED60B-3074-41B3-BAF1-1B7072917F30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ef0b7b1b961eba4f39a60242fc3f332f4da80e3","datavalue":{"value":"proofs-as-objects","type":"string"},"datatype":"string"},"type":"statement","id":"Q4276174$7C3D40DE-DEAE-4900-A44B-AF70F268EA85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q4276174$E075BF40-E3DB-409F-A3C0-C87FE8F26F32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4276174$A1A1F6B8-DB7A-4C4D-AB11-3C157CF32EF6","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":"Q4276174$B1F611C7-5C56-41F7-B4E8-C2600920CE04","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"180b07c0dffec29d5021dfdfe103efd21ecb48c6","datavalue":{"value":"https://doi.org/10.1093/logcom/3.3.287","type":"string"},"datatype":"url"},"type":"statement","id":"Q4276174$9BE5F05A-73F8-4BCE-B8C0-BE8B46C20F01","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b7b2e4a7a49576d07f5a4f974041fc7146c8c59f","datavalue":{"value":"W1969881696","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4276174$0A576C26-BF4C-4E0E-A51A-83C96F016D15","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dde6b3c960984cf71010c1293b95e685f86f9502","datavalue":{"value":"10.1093/LOGCOM/3.3.287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4276174$09F4228C-CF2C-42CB-9C6F-8A88CB074ABB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4276174$E1845BD3-C26F-413E-94DA-D8326424F714","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a3b5f35ffac738765229d207a551df6255c5ce98","datavalue":{"value":{"entity-type":"item","numeric-id":5958764,"id":"Q5958764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3b551a47c10f5041dae4b391a41e9016f628551","datavalue":{"value":{"amount":"+0.7753487825393677","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":"Q4276174$E83AA787-54BE-4BE1-894D-C6230F5D1CD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"050391e3f27b8bfab5af09f69bc4e968903fe067","datavalue":{"value":{"entity-type":"item","numeric-id":4871733,"id":"Q4871733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8402062c8985609fec34335e2b502bcfa76422f1","datavalue":{"value":{"amount":"+0.7690171003341675","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":"Q4276174$569C1956-3C96-4B0D-977E-0222C06D6AEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83ead96eb0dad59b33308a29c10c00c5949abf9c","datavalue":{"value":{"entity-type":"item","numeric-id":2723415,"id":"Q2723415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7cbe81eb32283c31c04862216f1944353c6b25b1","datavalue":{"value":{"amount":"+0.7637646794319153","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":"Q4276174$C3675FEB-8312-4B55-88B2-B5D64E7FA305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a08562885acdf630cb480dbe6bb784304badc973","datavalue":{"value":{"entity-type":"item","numeric-id":1868508,"id":"Q1868508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c957514f0bcb1788c9ee3d7fb0345ea5dde9efd6","datavalue":{"value":{"amount":"+0.7637643814086914","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":"Q4276174$B6E3B919-B42E-4104-B44A-7323389299FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c3243e05fe0fd1aebb4021426442c3380da6c2a","datavalue":{"value":{"entity-type":"item","numeric-id":5369477,"id":"Q5369477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b080569dd7f48356c0325bb6dc60e5de526c90c","datavalue":{"value":{"amount":"+0.7614902853965759","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":"Q4276174$3CB68267-A4C5-49E3-83C1-B1B706FD41E1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Complete Proof Synthesis Method for the Cube of Type Systems","badges":[]}}}}}