{"entities":{"Q6860025":{"pageid":20656783,"ns":120,"title":"Item:Q6860025","lastrevid":84252194,"modified":"2026-05-14T05:36:09Z","type":"item","id":"Q6860025","labels":{"en":{"language":"en","value":"Duper: a proof-producing superposition theorem prover for dependent type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8158251"}},"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":"Q6860025$05AECC01-A1A4-4813-A3E4-0DB77F91013D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c2f9d3dcd4d05cb7427e68c40ca5ead0ae9f5616","datavalue":{"value":{"text":"Duper: a proof-producing superposition theorem prover for dependent type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6860025$EF431922-BA1A-472A-8715-3E49ABAB537B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6c1ba7b8c03dc53949f800a4000a89825a8bb2fd","datavalue":{"value":"10.4230/LIPICS.ITP.2024.10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860025$9F197DF6-F1F5-4F9C-A17A-0105DB87273F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1e7a5be534fae34845b11c384a91520f8ebe70e4","datavalue":{"value":{"entity-type":"item","numeric-id":6860023,"id":"Q6860023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$D46C3D96-0123-4724-BD73-168F22AD10E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d3be9460201c3084f95da480f8ab39cb4abc576","datavalue":{"value":{"entity-type":"item","numeric-id":6860024,"id":"Q6860024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$51F22476-3500-40D8-AC6D-537B3743363E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"15de60d15cad4f16d9ed61faf6018fbe1d338db4","datavalue":{"value":{"entity-type":"item","numeric-id":1687713,"id":"Q1687713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$4BAD3CCE-674A-4F13-AD82-ACDB262B9E04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"834b9908deaa5f43ae5b55e2029a1dd9a50ccc06","datavalue":{"value":{"entity-type":"item","numeric-id":287376,"id":"Q287376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$6DE4A3F7-5209-46EC-84C7-0F10EDD15501","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f115c6be43614d2596ce7cf4daadf566de48c39","datavalue":{"value":{"time":"+2026-02-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6860025$81B774B2-1D2D-484F-AF2B-3AC78EC5B48D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860025$D016C686-685C-411B-BEB4-D5ED1D1F48C2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3ce7e0efb96fb03374dbb31c7b95eac16cbd9cd2","datavalue":{"value":"8158251","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860025$86AE583E-E8BA-4AF4-B70E-3E087B76ACED","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":"Q6860025$A03F45F0-3ED1-4EB9-BCC7-AE7DDDD61B6C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4879e8c35d56fd297a402f7c1eba53238e04d57b","datavalue":{"value":"proof search","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860025$C23FB93B-3E0A-4E73-A59D-71AD17388CE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d2aa687cef17cd912aad76972cec097c0540be8","datavalue":{"value":"automatic theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860025$59769620-AC43-4089-AB92-8DF67FBDFF0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860025$0B4F9309-623B-46C2-83F8-99368B890F53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860025$B620B66E-8404-403D-A2E4-D38C9128720C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860025$0E28079D-9810-420F-B22D-D892027F9064","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":"Q6860025$1B2E6B72-6CEF-4EC5-90BD-66A368CB0872","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$99C607A8-8C55-47C4-9801-D04B25AD0958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b248c9c4438a577886ba26fae36d944dd9eb1de0","datavalue":{"value":{"entity-type":"item","numeric-id":6156638,"id":"Q6156638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$16314E1D-8CE6-467C-ADF8-CD0CB09C4E74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9bbc9cdd9667523730b17037c3549c772dd39af","datavalue":{"value":{"entity-type":"item","numeric-id":5918381,"id":"Q5918381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$8CBE5FB4-803F-493C-8E2E-D5E951D292BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$60C350C1-B291-4EB4-B5CC-5EADD76C5F8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"961d1a3b466e06b467dc6809803cb8c6e25966d1","datavalue":{"value":{"entity-type":"item","numeric-id":6492729,"id":"Q6492729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$874D69A1-6DA7-4A1D-9EAC-ED8363EE2831","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ee178f7541c5d2ed1d6ee17e1e99ce6d2d8a20c","datavalue":{"value":{"entity-type":"item","numeric-id":5195271,"id":"Q5195271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$FF832E41-F85E-481F-8DD6-BAECACE0D095","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$E0693CB9-2639-4999-A6B4-96AE399A703F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"112a3ea35e000d8c0e7bd315e341f66faa230a1a","datavalue":{"value":{"entity-type":"item","numeric-id":2305410,"id":"Q2305410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$52C1D99F-9954-4F97-828A-43E9F3E9DCBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49ffa08056b25c8397b28a5c628da1ed39b7b155","datavalue":{"value":{"entity-type":"item","numeric-id":6642984,"id":"Q6642984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$2413B199-0644-43FC-A62C-0A81FDD088DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ed2462edf5f32ab2aaa354ff9ecbd66b037a97f","datavalue":{"value":{"entity-type":"item","numeric-id":5048991,"id":"Q5048991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$393D2D6C-85CC-4AE1-A398-CA483A484FF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd3cb6b9019747c7bbfc2bed55b78e42a7665495","datavalue":{"value":{"entity-type":"item","numeric-id":1663240,"id":"Q1663240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$72FFB77B-D779-4EC7-824B-0733D4555BB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"432347ebf7758fa5347be4c601bf2d08f68cb652","datavalue":{"value":{"entity-type":"item","numeric-id":2055901,"id":"Q2055901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$98235DAB-B421-4665-BC86-0065ACACD741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bac46cadd391b69a8eb2eb17270bc333130444c","datavalue":{"value":{"entity-type":"item","numeric-id":6572540,"id":"Q6572540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$CD3E50BA-B275-4853-866D-5D3BA5FEE784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3bc6dfc633db1b802a1487f9064ea79563c34bf","datavalue":{"value":{"entity-type":"item","numeric-id":4046035,"id":"Q4046035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$B8D2A4CB-A18F-423E-A41B-72592509F3CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9811e0f445518a60fcf8a88a2ec5cd76d23ab843","datavalue":{"value":{"entity-type":"item","numeric-id":5477649,"id":"Q5477649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$70FDB9A1-4F2E-4A26-98B6-39565EF60E7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"014df434e19c98aa84979531cf42f2d47588711c","datavalue":{"value":{"entity-type":"item","numeric-id":4647531,"id":"Q4647531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$C54C558F-B517-448F-83CE-48B942A98B1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93c550078709a24810b3ec6e1d82a47c85cb06a5","datavalue":{"value":{"entity-type":"item","numeric-id":2018657,"id":"Q2018657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$D835D193-731B-4E09-9FBD-625CB69EA793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e14549321cbae3c57ae9ce6a9266b4af3d64fd4f","datavalue":{"value":{"entity-type":"item","numeric-id":286800,"id":"Q286800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$2C877E40-0E5E-4AC4-A39E-D95AFD349399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$DD767863-6960-4797-8360-F6C11773031B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"005a359e0c4194dc29e9a7f915c69fa31db62513","datavalue":{"value":{"entity-type":"item","numeric-id":861708,"id":"Q861708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$346AB5D3-A9D4-4319-B323-970482AD69BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f38c339bbd571c9f13a1b3052c0abde7b640b4a","datavalue":{"value":{"entity-type":"item","numeric-id":2471742,"id":"Q2471742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$68304540-8107-413B-94A2-2405F2A65637","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"741b1c2a1697c669d1b3bbdff87dd79f9f007366","datavalue":{"value":{"entity-type":"item","numeric-id":1006731,"id":"Q1006731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$580E2EFC-5D78-4C28-A324-83E95890A717","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d120742af8436a54e9c640ab06706d350dfdb2b6","datavalue":{"value":{"entity-type":"item","numeric-id":909488,"id":"Q909488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$5BAB7909-4649-4D04-93BC-7E0A77E3265E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42ba0d7a787c3ddf27f1ee78a59c4dec37184a75","datavalue":{"value":{"entity-type":"item","numeric-id":4520767,"id":"Q4520767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$2A4467A7-287A-46C6-B27F-B52C3751A2F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"716d170b6d9b095492bf0c2b742ee0dbade5bbe0","datavalue":{"value":{"entity-type":"item","numeric-id":3523178,"id":"Q3523178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$D2C44019-B755-470A-B49A-4B8BB2FADE1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$084FC510-6799-4CED-A2C8-3ACC51255F2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9055b0cc60b35ae226978f59203587ec6cf2e814","datavalue":{"value":{"entity-type":"item","numeric-id":714712,"id":"Q714712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$AAE5BADD-A5C9-45A7-9B08-5CF6D5DD8E20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ae658c7b9ce655f09bbbbf265b43c9366e7c7d1","datavalue":{"value":{"entity-type":"item","numeric-id":5145460,"id":"Q5145460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$DC922AF9-A6D8-4D3E-928A-38671B3AAF05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87010eeb527e471d8b5efa91a72d28a4d17b16f0","datavalue":{"value":{"entity-type":"item","numeric-id":5019796,"id":"Q5019796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$56AFBD23-906C-4D93-BB99-DAC00889A67E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30ea05e6ba45e2c68d92f5c8b742132b4d21f715","datavalue":{"value":{"entity-type":"item","numeric-id":5069650,"id":"Q5069650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$FE6E5645-5235-4775-B235-512BAD0AB25D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"775c0fbb82731a41620bf40f868b011533300a54","datavalue":{"value":{"entity-type":"item","numeric-id":6200767,"id":"Q6200767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$F1AE9B76-1BC8-4983-8F27-6BC30B7CBBE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89bb690d82158de9c3d7b82fa1b8420468715e47","datavalue":{"value":{"entity-type":"item","numeric-id":6095787,"id":"Q6095787"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$68EEEF0A-8D33-4D9C-8209-E29F1D5DF243","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59d69e7c781c6370212654a029921d34ee26dd92","datavalue":{"value":{"entity-type":"item","numeric-id":5918403,"id":"Q5918403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$8C11BEF4-18AB-4964-950C-F704CCA21DBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd64358c68335b8f55c95884438c93973af5783f","datavalue":{"value":{"entity-type":"item","numeric-id":5028439,"id":"Q5028439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860025$9EFB39DF-0732-4F8D-845B-13069DE0F808","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Duper: a proof-producing superposition theorem prover for dependent type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Duper:_a_proof-producing_superposition_theorem_prover_for_dependent_type_theory"}}}}}