{"entities":{"Q2362206":{"pageid":2372949,"ns":120,"title":"Item:Q2362206","lastrevid":72597651,"modified":"2026-04-14T05:59:26Z","type":"item","id":"Q2362206","labels":{"en":{"language":"en","value":"A fully automatic theorem prover with human-style output"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6740419"}},"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":"Q2362206$96A093CF-BFAA-4E6C-ACED-DF2ABC87BD25","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"425c6ed27ce908a2535a0236c5d96a9a9aeaac11","datavalue":{"value":{"text":"A fully automatic theorem prover with human-style output","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2362206$8FFB66B5-5F05-4543-A35D-3729B470024C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c375676f645788b5a39e9246e5c1ec6be9f90dd8","datavalue":{"value":"1405.03035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362206$3FCC9567-6AA6-4812-A76E-6321420935E1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"389bac30a129091023a88c2c3d6f552ab4415e5d","datavalue":{"value":{"entity-type":"item","numeric-id":1940485,"id":"Q1940485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$C3A0471D-98FC-4D84-A3B7-510EF82D086D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4c6ea64cd33947bfa46f02702a3c99f04fd132a9","datavalue":{"value":{"entity-type":"item","numeric-id":237986,"id":"Q237986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$8C31F3E8-B0E2-49AE-A80B-5D39DA7A0054","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":"Q2362206$631AFE3F-9B99-4049-B974-189DBE2B2AE6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1a7c9d02f6a4a594410711d22dd1a021deb4336e","datavalue":{"value":{"time":"+2017-07-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2362206$3740D963-31DF-4EF2-A74A-B984CC52E5E2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362206$7F624BB8-F7CD-43B8-AF8A-B8ECAC62D893","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362206$3E812071-E2C2-489F-8C46-8BDDD0D4A64A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dbbbe1e7d397378365a308afb963021a7323a3d6","datavalue":{"value":"6740419","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362206$18FC982C-0C8D-42CF-AEAE-D7D7E6F9DC11","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3640b5395457c8e78cd0865e114c80a8efc0e4bd","datavalue":{"value":"ATP","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362206$154388DD-5385-474D-A35A-946C66AE2FA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362206$04A43BD6-EC79-4591-9030-2AD5DE1664CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a9bc600d540813bb8d86ed09e6b6d2a7569b6ebf","datavalue":{"value":"human-oriented","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362206$3FB7DA64-6AA5-4CB5-BFC4-9A32601ED9C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df27816c0a4ff2e31fc6cba750fea130947311b9","datavalue":{"value":"human-oriented theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362206$3766F88B-07E4-4964-900D-52CCAA879642","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2b4970b7eec7fe74567d7726d90ad3f7dc5ae6b9","datavalue":{"value":"human-like output","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362206$35E2692E-85A8-4C01-B439-61994DEE15C6","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$4804B57A-8848-4FD3-9104-80104C834EC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91b852acc0d0dcb394ea74c8e76a901ae0257702","datavalue":{"value":{"entity-type":"item","numeric-id":21776,"id":"Q21776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$44BB0240-AFE5-440B-B730-1223A920E1C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bab752e9cf98240487eb3aae10666dc541b36d41","datavalue":{"value":{"entity-type":"item","numeric-id":43692,"id":"Q43692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$0A25E534-CF47-4A37-BA4E-D71C7F09D788","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"29391b19386946f3f8609d95651483db905027b9","datavalue":{"value":{"entity-type":"item","numeric-id":22439,"id":"Q22439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$FE5DBDEC-28B1-4EDE-A91F-B74328F655F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"31d2ddeef485fccfd3a5fe32ea329d2b65b4f1b4","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$598A64B6-A7DA-4A40-881D-1D1EB4503C1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dec9660857c05980e3c0b17c51d483bf1a29e419","datavalue":{"value":{"entity-type":"item","numeric-id":40021,"id":"Q40021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$2BE45F38-C6DA-40F4-A2A7-0961A7FE2FEC","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":"Q2362206$6DBA3EDE-FBE7-4B8F-BBA5-99265C7B727D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"182ce6485eabdb85778a522def34fa68409a7c10","datavalue":{"value":"https://doi.org/10.1007/s10817-016-9377-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q2362206$EC940FC4-286D-4708-9D01-139ED10F6F00","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"afe458d1ae4bdc1133ea32261e227e40d37b6811","datavalue":{"value":"W2413604966","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362206$C2CB3702-EF52-41AB-A118-A9C18E073613","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ae479902f939a8da2fc0a0a3d500956619aecf5b","datavalue":{"value":"Q59615366","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362206$6C8F42BF-4A7C-4688-90B4-F38FD18DEC97","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce52b549975f2f1eb2794b7e93bf906aadaa4ff7","datavalue":{"value":{"entity-type":"item","numeric-id":4131708,"id":"Q4131708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$CEFBE8F4-D363-4A8A-AA6A-FDCFBEA8D37B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0a919e94eb05990dfa452cda990dbe76002728","datavalue":{"value":{"entity-type":"item","numeric-id":4217949,"id":"Q4217949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$07E06209-D25D-4348-8C09-85C9909D65A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9246a891b5d36ce51ed599b16ca1ffb87244abc3","datavalue":{"value":{"entity-type":"item","numeric-id":5950931,"id":"Q5950931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$CA0CEA2A-A0E7-42F2-99C3-2B33CAD28BCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f20e02bb907f90cb22a0a676f448fd7139f7410","datavalue":{"value":{"entity-type":"item","numeric-id":2547495,"id":"Q2547495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$F202C810-2ABF-4740-B687-B94A0984BA0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e857e95d91a8e9f3746c9aca423c534197fa21d","datavalue":{"value":{"entity-type":"item","numeric-id":1238434,"id":"Q1238434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$E505215D-09FF-4424-8AF6-E34BA2A98558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c737ab66b5212371b2af0c3c73412bd0e833013e","datavalue":{"value":{"entity-type":"item","numeric-id":657585,"id":"Q657585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$5DCD99CD-E0BE-4CB8-AF48-F73A4196B997","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2330859a81aa2a457c43250fa16bdebe82a1da52","datavalue":{"value":{"entity-type":"item","numeric-id":2554244,"id":"Q2554244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$72D9C71C-78E9-4D32-9804-48D85AB151EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$80CF8DDF-0BA8-4013-A0BE-973A619C9EAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7e013849775846918727fac3e7e6455bd448813","datavalue":{"value":{"entity-type":"item","numeric-id":865646,"id":"Q865646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$06CE9F3E-7FB1-4FAC-BD01-1102EBAB8C35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a9656f101a9d31950a102f3d80db35fe042a1cc","datavalue":{"value":{"entity-type":"item","numeric-id":1940486,"id":"Q1940486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$6449B037-2E74-4A5B-A15A-3FC5FC14DD87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"545b70a52fbd739fcbdc5fb79649e5d3315f9433","datavalue":{"value":{"entity-type":"item","numeric-id":3598006,"id":"Q3598006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$1E977677-42CA-44F0-9A10-DE2F25D0CC7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dac16af6cf1adb18d0516e2c8db27f45fc424e6","datavalue":{"value":{"entity-type":"item","numeric-id":5327343,"id":"Q5327343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$1E464589-F731-435D-AE26-1F27FC3C50FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb4857d0d243b746647a153e1690cd4acc84f69e","datavalue":{"value":{"entity-type":"item","numeric-id":5280247,"id":"Q5280247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$E50FB4A3-F39E-4895-ADC8-C2F769462AF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3dd33855336399d060e4c0008afb085c9559eabd","datavalue":{"value":{"entity-type":"item","numeric-id":5747782,"id":"Q5747782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$ED1A14D6-B101-4B1C-BC70-45660329F755","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d34d9b1e4e7ac9abe6effd9d10da2be3e29dc93b","datavalue":{"value":{"entity-type":"item","numeric-id":3600462,"id":"Q3600462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$47656285-534F-4B6D-B56B-34237392F05A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"777f1902a1127b94884ae1ddc89768860f054a6e","datavalue":{"value":{"entity-type":"item","numeric-id":3789060,"id":"Q3789060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$0D0264DB-915C-4950-856F-A6E13870E9AC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"75ef2db9f847cb402a6ae42940c05c0ab5a01fa0","datavalue":{"value":"10.1007/S10817-016-9377-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362206$7F14F365-02EF-4153-9AF9-6A7AE216E194","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c464355e162bb39742d35675ae4f88b3e02fa0d","datavalue":{"value":{"entity-type":"item","numeric-id":4370791,"id":"Q4370791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c3e188bb05aff3ee8ffceb272ac4b0e4ed097aa","datavalue":{"value":{"amount":"+0.7701834440231323","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":"Q2362206$10E87B95-0DB8-4A71-8E7D-E8F76F1F50C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b53fd36785de4a96164f555f93c3baf017fceaf3","datavalue":{"value":{"entity-type":"item","numeric-id":657585,"id":"Q657585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f87da4e3091686171cc951c08d446f2a62cb8921","datavalue":{"value":{"amount":"+0.7669079303741455","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":"Q2362206$D32A15B6-F1EC-48E1-87CC-600853DB0D6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2565d9e77d9b51b905daa5bfbb63ce859f62d93b","datavalue":{"value":{"entity-type":"item","numeric-id":3345811,"id":"Q3345811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec8c85cba69482de2f25dee254af4042bdfe6a6c","datavalue":{"value":{"amount":"+0.7554132342338562","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":"Q2362206$BE7E9321-FD7A-4035-A4A5-DDF0A939C749","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d49d4c6bcd3850ac8d47bcd908e5e333fb490b4","datavalue":{"value":{"entity-type":"item","numeric-id":3006508,"id":"Q3006508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53039c430d9fb56d2d44e5f103ca19d0af6dad39","datavalue":{"value":{"amount":"+0.7482043504714966","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":"Q2362206$1064733A-1820-45EC-A9D6-92050C12187E","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":"f5af53b7ab57dfc23fe6971234390b3d990e1c56","datavalue":{"value":{"amount":"+0.747792661190033","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":"Q2362206$EC1AC6B6-6A4E-4E67-B99F-EF0A80B36C9A","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362206$4E60B91C-B7CB-4DF6-BAFB-72853651CCD4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A fully automatic theorem prover with human-style output","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_fully_automatic_theorem_prover_with_human-style_output"}}}}}