{"entities":{"Q1868508":{"pageid":1879250,"ns":120,"title":"Item:Q1868508","lastrevid":71020188,"modified":"2026-04-13T18:57:44Z","type":"item","id":"Q1868508","labels":{"en":{"language":"en","value":"Automated proof construction in type theory using resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1901556"}},"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":"Q1868508$6437B9B8-B961-4983-8CE9-DBEFF8367F43","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f609e72dbc517c4618929c172394c3bf38ee0eb3","datavalue":{"value":{"text":"Automated proof construction in type theory using resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1868508$16B6DD5D-D918-4FDB-8854-62B3AA57CE0C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7651d317a249efe0927c6f3d960109504b561cc6","datavalue":{"value":"1015.03018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868508$5C78C7B4-5DF6-45DB-8E70-FCFEA971AD73","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e109eaf5f6caed9b7ca9a3c59a16f39e6d085050","datavalue":{"value":"10.1023/A:1021939521172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868508$64A95D1C-4E2D-48E6-A06E-BD55B5B568CA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"86dd1292a8b5a1afaa94642cc6a7d0169c59a759","datavalue":{"value":{"entity-type":"item","numeric-id":409313,"id":"Q409313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868508$E5012795-CC87-4944-BE53-E885165A9E04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3ca9aba1d27cc0a527c5e55e40b675c206cdc1e1","datavalue":{"value":{"entity-type":"item","numeric-id":549187,"id":"Q549187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868508$C212BFD3-CFD4-44F3-A673-E6E88C7F7EFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0af7e025189305bad11f686c710fe3b187470eaf","datavalue":{"value":{"entity-type":"item","numeric-id":438567,"id":"Q438567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868508$3859B8DB-0114-4241-818F-0CC877B498D8","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":"Q1868508$B2251AEC-E3DA-486F-A46E-6FE1297EA519","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ae7235402c0b574ed2e2213feb9e21452b645cac","datavalue":{"value":{"time":"+2003-04-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1868508$A2011567-2AE9-4B37-84F0-82171531A596","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868508$CF264C8E-0ED7-480B-9EAF-D220919E948D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868508$AEAAACD2-A82E-43E5-AC04-5B1EE36BFB5A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6524d9d0db6c80422ef1da97c4bc30fdc1bbc324","datavalue":{"value":"1901556","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868508$06629517-00C4-4918-87BA-D6C5F486BD4B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868508$7D0E029C-CA0E-4065-83FB-B25FF37F1ED7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ebcb3e967d7f344660d4e6719070e8abab46ff77","datavalue":{"value":"proof construction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868508$370C904A-06BF-4CB6-A475-60756E1B9C57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03158307b01a6e2de96f5585d7a65d8e1a522aae","datavalue":{"value":"resolution theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868508$48EE800E-AD43-4EEE-B51F-27A85DD27F2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01f639a56e1e38a2490c4463ce011c878a3d36ab","datavalue":{"value":"typed lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868508$D8657F7A-4FDF-4358-B2F2-97EA611CBE9B","rank":"normal"}],"P1463":[{"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":"Q1868508$7C5C2D71-B8AF-48A4-8082-399F908AC5F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f028a8a6db3bc5ae4579b69f24eb8d66b93659f7","datavalue":{"value":{"entity-type":"item","numeric-id":31448,"id":"Q31448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868508$DB725879-98EF-4D97-B625-2539B24F1764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4a761178b05ceb8505a589f51ea41c7640322dd0","datavalue":{"value":{"entity-type":"item","numeric-id":33154,"id":"Q33154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868508$0A0B01E6-A019-42A1-A989-A39F3D780669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af3b5ddb4818ec81bb9bea3bab4852742bff1bd5","datavalue":{"value":{"entity-type":"item","numeric-id":22101,"id":"Q22101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868508$42F265E1-D145-4482-B02E-6F3C8910A0D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"233bd03fc74bc4c01e6f828569e5eb13f94bb747","datavalue":{"value":{"entity-type":"item","numeric-id":22242,"id":"Q22242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868508$6108230F-05D7-4E58-9A79-FB6648A81529","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":"Q1868508$5A17E30A-44AA-4F0E-A604-70100BE1ADE1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a1335d6f3d89534dc5ae417acc6cf5ccf0474753","datavalue":{"value":"https://doi.org/10.1023/a:1021939521172","type":"string"},"datatype":"url"},"type":"statement","id":"Q1868508$F903CECA-4F97-4FCC-8733-4D70E45AABCB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a4187646f447e904ad7636ddbf4c5b780697cc94","datavalue":{"value":"W2168281995","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868508$5E65B7C0-538B-48FD-8223-3516F61AC127","rank":"normal"}],"P1643":[{"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":"cef9350d42bb16fc96bf85b1eb1eb164c9423481","datavalue":{"value":{"amount":"+0.9982748031616212","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":"Q1868508$8C7B69A8-8ED0-4C6C-A344-2253AD2465CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97650e096cd8fc874b01c43330063955389b285b","datavalue":{"value":{"entity-type":"item","numeric-id":4720797,"id":"Q4720797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c0808792d163bcbdc92b36a4775852c2935d4f1b","datavalue":{"value":{"amount":"+0.9982746839523317","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":"Q1868508$ABF28941-639C-46A1-9F8B-1DB45F5D6924","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbeb9544776f1dc6173f1eefae3f367964f2f759","datavalue":{"value":{"entity-type":"item","numeric-id":4012878,"id":"Q4012878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"618ed9ea8d07f4b3b98eccc9015affbb73afcf3b","datavalue":{"value":{"amount":"+0.815710186958313","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":"Q1868508$BFA0512C-C754-4AD7-AFE0-5740A14019E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e39ac3ee7536d87b921b90eac5d0a3e6e1167fd","datavalue":{"value":{"entity-type":"item","numeric-id":4276174,"id":"Q4276174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a78149781a6fe441c2cbd979c6097386271f712","datavalue":{"value":{"amount":"+0.8134200572967529","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":"Q1868508$B3DFB22E-4422-46FF-A3E4-5085170FD6A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b5fe89c802bf99e3b7d049a8d7c4d9ef2f2e9a0","datavalue":{"value":{"entity-type":"item","numeric-id":4503899,"id":"Q4503899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"233054d98160ac134cadc1a98be0159603167b5e","datavalue":{"value":{"amount":"+0.7891010046005249","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":"Q1868508$E7B96CD2-D056-48DA-89E4-7EC045ECA99D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated proof construction in type theory using resolution","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_proof_construction_in_type_theory_using_resolution"}}}}}