{"entities":{"Q3295156":{"pageid":3305864,"ns":120,"title":"Item:Q3295156","lastrevid":45893512,"modified":"2025-12-20T02:16:49Z","type":"item","id":"Q3295156","labels":{"en":{"language":"en","value":"A Mechanized Proof of Higman\u2019s Lemma by Open Induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7218747"}},"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":"Q3295156$20CA9B30-1BAF-4E8D-98A4-F883816E228E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"40a21c1be4e274c7311b1d078d558852529e6e8c","datavalue":{"value":{"text":"A Mechanized Proof of Higman\u2019s Lemma by Open Induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3295156$1DBBEB01-3FF3-4608-AE71-F1E40C4ADEF5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2099ce1e95d9ae1011679d98a84f24329a712253","datavalue":{"value":"1446.68188","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3295156$4BF8BA3A-FC94-4700-8847-9ACD348225AF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7e1ecf270d8c8fd744715ae770b2052003e68b47","datavalue":{"value":"10.1007/978-3-030-30229-0_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3295156$E0F0107A-3FBC-453E-95BA-A9CB31131F95","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0653fc883593f9e70c5ddda3d1f1f752c0d0ffca","datavalue":{"value":{"entity-type":"item","numeric-id":530846,"id":"Q530846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$7655722B-DC27-4DF6-95D6-77C4039197C2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9ef5f862067a8dcfef6601f996709bbb53d732cd","datavalue":{"value":{"entity-type":"item","numeric-id":3295143,"id":"Q3295143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$0580FF4E-4DB5-43C1-8F73-3DF5733F1161","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7a00d12a888ce0ffc3aa72928c7254f31eb87f77","datavalue":{"value":{"time":"+2020-07-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3295156$5129416E-9178-4A71-8F15-AC6CC24746B7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3295156$A9769E1E-C20E-4054-800F-1920BACFE35D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3295156$5747AB2C-56E2-45BD-BFCB-7CB2516FF005","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"da00c812255bd7f02dddc14c65a56e042cf0446e","datavalue":{"value":"03E05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3295156$E14E4485-1D1D-4903-8870-714AA55075CF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"de2fc7bcb1ad96f88e10621881ce8f1ce67ff7be","datavalue":{"value":"7218747","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3295156$314B875B-7A3D-4283-8105-A61C49935D8C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"79e3d96b80d97b60f7420ee39a9ac16a248efabb","datavalue":{"value":{"entity-type":"item","numeric-id":40319,"id":"Q40319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$62D6309F-1272-41D6-BFA3-5257ABDA51EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0ef0ca4e812ccc71b1750f838c7d82339bf64c7c","datavalue":{"value":{"entity-type":"item","numeric-id":41247,"id":"Q41247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$C4E9F292-2F5F-46C0-8134-A1C124EB24E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$30E3F094-02FA-4425-8D2C-0D53BCF8DEFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8e7deacad56e3bf59f522de6c1fa96858f2fd494","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$F07CDDD5-058C-4B65-8648-6F5969928A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$1CD21B13-5E3B-40CC-9B38-A8E5B26BDB71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d758ac0ae837e1988fcbce179d850d4d45b9dad7","datavalue":{"value":{"entity-type":"item","numeric-id":53718,"id":"Q53718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$AD23D67D-4B4B-4CFC-BA3B-01A1FD350ABC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd1392891407fd9f11bfc5ced5f71a7f7a0fb2a6","datavalue":{"value":{"entity-type":"item","numeric-id":40261,"id":"Q40261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$BFEFAF24-C586-46A4-BCF8-3D30B4C07FE5","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":"Q3295156$CB50F585-375B-4CD4-9CED-BF9A3256B313","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6c915b8ff48ed40febb28d5de60010cb52192213","datavalue":{"value":"https://doi.org/10.1007/978-3-030-30229-0_12","type":"string"},"datatype":"url"},"type":"statement","id":"Q3295156$63DAE362-5750-4531-A285-D9F34787F126","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"55b0e444f1c23db04fdadb6dd7e79e098fd28387","datavalue":{"value":"W2998676580","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3295156$D5C68F43-CEFC-47DB-B10A-6B2A0D9523B6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"eeddfec2d6761bcca5b706cfa4f21836083ab429","datavalue":{"value":{"entity-type":"item","numeric-id":5712322,"id":"Q5712322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$A5EF88C2-FDF5-4DF4-B259-5F261CCD3288","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"274736e3c02109cf273cdf7bf9017ac1fe6ca469","datavalue":{"value":{"entity-type":"item","numeric-id":2958383,"id":"Q2958383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$22234A2D-BEFA-492F-AC60-BFE842AAFE16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b977cc0abbb9233e203718261068766885e4fb3","datavalue":{"value":{"entity-type":"item","numeric-id":4246946,"id":"Q4246946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$EAE54132-461A-4991-97F7-5AD831D47A69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58709679cfff7718457ae5dbfaa34a4e9b17219c","datavalue":{"value":{"entity-type":"item","numeric-id":5812263,"id":"Q5812263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$A167B767-5D00-4931-A139-C8BDEEC91CE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11e5b43c5f0e711ef91c4f8e7255199d25558fbd","datavalue":{"value":{"entity-type":"item","numeric-id":5541375,"id":"Q5541375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$7BA36720-1E9E-4C14-8937-6634165B2F57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c57448c3511c30ed92e5fbbbe68c6f2b95237a20","datavalue":{"value":{"entity-type":"item","numeric-id":2554710,"id":"Q2554710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$4EFF539A-D07B-4B76-A903-DF7B1FFA708C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ed0853d5d25943754f0b88d3bc5a4e688b584cb","datavalue":{"value":{"entity-type":"item","numeric-id":5734436,"id":"Q5734436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$7CA3E642-6E7E-4764-B068-8728039CACC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$5EE7BF41-0D21-458A-9C88-C659DE9352EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf1e6e74fc9f0e43b2bb5ebeafd488ad5919a3c3","datavalue":{"value":{"entity-type":"item","numeric-id":1112816,"id":"Q1112816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$CBDDE388-B230-40E3-B25C-155013994317","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20d8ad24cb4bd25b66b08a8a88a01461662f8272","datavalue":{"value":{"entity-type":"item","numeric-id":1803588,"id":"Q1803588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$95CC8951-F872-41D5-B446-A5FC199D0286","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed201b22ef1a4e26ab767034f85a72d6913cb4a0","datavalue":{"value":{"entity-type":"item","numeric-id":3305561,"id":"Q3305561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$A6472DC8-318F-4CE9-A5A2-3417307A978E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6f8ba04e25c8e53833bb5d22263f9a05336ea6c","datavalue":{"value":{"entity-type":"item","numeric-id":5195254,"id":"Q5195254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$053FBD8A-EF8D-4590-AB03-8136AC461B46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6a03213b095a350f4bf2d8dc4d804066ee4390f","datavalue":{"value":{"entity-type":"item","numeric-id":2958390,"id":"Q2958390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$2D7801BA-0275-4FEA-89FC-D740E64427F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$47238610-D2EF-46CB-B962-218F89F855C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ac1ee249c73c16d45e6922836fb575790a28b14","datavalue":{"value":{"entity-type":"item","numeric-id":3353014,"id":"Q3353014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$E47C6DFE-A0BF-4B2C-9882-B91A7B6A56FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b16e98f2ed75b6b2c580aaaf672acd628aa682d","datavalue":{"value":{"entity-type":"item","numeric-id":2914747,"id":"Q2914747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$85EB5923-A21D-485B-B5EA-0F12B14712D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dce670ec1d34ee6c61f1437c968abe3b27423157","datavalue":{"value":{"entity-type":"item","numeric-id":3088018,"id":"Q3088018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$99C5E4EE-F8FA-4F6C-A6B1-8D9A43A4E215","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae619157034cd1b5b5d2d2ffdf596718f766a9dd","datavalue":{"value":{"entity-type":"item","numeric-id":2351151,"id":"Q2351151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3295156$3F03C148-D587-43A6-A713-FCFFBDBF08FD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3295156","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3295156"}}}}}