{"entities":{"Q2851941":{"pageid":2862661,"ns":120,"title":"Item:Q2851941","lastrevid":83869544,"modified":"2026-05-07T13:05:36Z","type":"item","id":"Q2851941","labels":{"en":{"language":"en","value":"Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6213572"}},"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":"Q2851941$F6426497-03D6-434B-9E2F-A933B7116440","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aaa26a8b764d40693ea2fe7ffae8337eb26bffdf","datavalue":{"value":{"text":"Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2851941$BFE40F9D-E298-4045-9BE2-5D6F709DEE97","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"457eab1c465d8c2b426f3a9335d009b3d3fffdeb","datavalue":{"value":"1401.68277","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851941$61E4E638-DF4A-445B-91E4-32D42EFFA319","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3191b2c066fd6af382494e9cd122a2a5a154bda2","datavalue":{"value":"10.1007/978-3-642-40537-2_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851941$81B78D32-1911-4A09-BFF9-B64BEA4637DB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a6be8d909a46685b6a24cecd253b3dd33cd2a6cb","datavalue":{"value":{"entity-type":"item","numeric-id":832718,"id":"Q832718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851941$C8BA95E0-A058-45CB-9426-0631876C3661","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851941$DF1177E4-7230-46D3-81BE-F4CB29AE0984","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1145dc38b4d246480a51682f22dd7d8a161033fa","datavalue":{"value":{"time":"+2013-10-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2851941$F40E7272-C159-4BB1-A387-C43564272566","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cad212f0caf0d22abf379c92f650fdaac225c7b6","datavalue":{"value":"https://hal.inria.fr/hal-00906789/file/Psyche.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2851941$26078BC1-9FF0-4A1C-A45C-2E0C165F83A4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851941$254E678F-99F7-45AA-BD04-819C5661559C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3ad83701931f155b21cbe696a001bb621613bddd","datavalue":{"value":"6213572","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851941$99DA4341-CEBC-497F-B213-25A61EDFF6F7","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":"Q2851941$782A9653-644F-46FB-8C32-8CA39854196E","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":"Q2851941$8A02E02D-845F-4614-87E9-085824CCECE2","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":"Q2851941$D5C80568-8FCB-4CC1-874B-6610D637C59F","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":"Q2851941$C9790418-B48C-430F-BED9-C45A95B8CB26","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0e75d4213992e449bf179468dacb7e56c8a88e59","datavalue":{"value":"W2208061263","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851941$D5DC026D-D285-436C-B3E3-30C971183FB4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b531c3034b1b9d2802c2c93a1364c959e1e20094","datavalue":{"value":{"entity-type":"item","numeric-id":2964465,"id":"Q2964465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3173a7740c216191a5eab01eb9a26cda7242304","datavalue":{"value":{"amount":"+0.7136186361312866","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":"Q2851941$4B03E2F5-24F0-4311-ACF1-56449973EE7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b97ad471e6172b61acd1f2b10b8e40a3cfe9a5bc","datavalue":{"value":{"entity-type":"item","numeric-id":3003307,"id":"Q3003307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03318d26afb38cf45d68fbb086cdf4aabbbd42f1","datavalue":{"value":{"amount":"+0.7002437114715576","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":"Q2851941$934C025C-54E5-4324-94A5-F7095A9CFA6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cc628ec77f4225c1666946ef50ea6e3eddd77d4","datavalue":{"value":{"entity-type":"item","numeric-id":2754047,"id":"Q2754047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0ac5c95bbc4434ae876b5b9f8b1fd22e8082c15","datavalue":{"value":{"amount":"+0.6968589425086975","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":"Q2851941$74792F0D-2456-4023-9E31-DA99304EC1A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8ba6d19053d2d5a1a4c519a0995a0629d3a84cf","datavalue":{"value":{"entity-type":"item","numeric-id":5747767,"id":"Q5747767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"203d5ec890e73286fd72bedc8580c8a9dee709ac","datavalue":{"value":{"amount":"+0.6943053007125854","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":"Q2851941$42A0FFB4-4147-45A8-874E-BA97456C561D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d515466375177240c9a5a9d2e20b70905c14b4a","datavalue":{"value":{"entity-type":"item","numeric-id":5376325,"id":"Q5376325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"802db73c4f66f35bb9e0840101aed2de1a6b2101","datavalue":{"value":{"amount":"+0.6891947984695435","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":"Q2851941$9FD67292-0D01-4714-8158-AC79CCC96000","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Psyche:_a_proof-search_engine_based_on_sequent_calculus_with_an_LCF-style_architecture"}}}}}