{"entities":{"Q7025183":{"pageid":21653997,"ns":120,"title":"Item:Q7025183","lastrevid":77543573,"modified":"2026-05-05T04:01:30Z","type":"item","id":"Q7025183","labels":{"en":{"language":"en","value":"Herbrand's theorem in inductive proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7986599"}},"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":"Q7025183$B783461B-2F91-4FDA-A9DE-27A10A2881A2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"171027e8f7f05616fb5db3ec431526d8579183cd","datavalue":{"value":{"text":"Herbrand's theorem in inductive proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7025183$AB15BF2C-E8D9-4239-B663-7AEAE6AEE8A2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ba71775c71fe4124bb904909da9e1c20f3ae94c0","datavalue":{"value":"1564.03026","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025183$66736B48-F65D-4116-A5E5-B960BE043C62","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b0cdd1c8aba00feb4474e652d1a88a94250351a4","datavalue":{"value":"10.29007/DWDF","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025183$ADC9F297-90A1-431E-83AC-55FD5D8C2D7C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"53993ae6db4350dacb1d3d4f5370b18b73e58da6","datavalue":{"value":{"entity-type":"item","numeric-id":167060,"id":"Q167060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$2469B79D-5783-4828-A457-10A27AE7A2AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e0af247aeda0d0aefbfde68ae92601a0a6b67c69","datavalue":{"value":{"entity-type":"item","numeric-id":670703,"id":"Q670703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$D67263F7-BA76-4B6A-AE5B-5591FE997A43","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d34a2e6c4099712e6f2a5acfda08782bd5ee66f2","datavalue":{"value":{"time":"+2025-02-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7025183$F4339E68-FCDC-4630-B1DC-9BBA5B86761F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025183$917C9F1A-245F-43C4-81D7-AB2385267FC6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"33ed0c4e9d0f138b86c53090e9f321fa6c8133e7","datavalue":{"value":"7986599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7025183$3FBA5F78-D510-446A-BC9E-E9A27B184BA5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9f8835bea84ff2121e8f066deb84ed12c2bf2d1f","datavalue":{"value":"Herbrand sequents","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025183$9ECC4E31-FEBF-47E1-A459-F0C8606D17FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac51fb7fe1eacbcc34c109a96dfeb7f186a8cd37","datavalue":{"value":"inductive proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025183$0208A33F-0C90-41B4-9A8E-9F0DE977AA9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"903ba53cac2857e1960af58b562e2d7b7717580a","datavalue":{"value":"proof schema","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025183$611B5E79-32FC-4A7A-ACF4-AADDD4AD5C94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73a0cf77ac822c82f34614cd0b3bf097336e98b1","datavalue":{"value":"resolution calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q7025183$E88AD518-7DD0-4A06-A9E5-B72F7C14BCCD","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":"Q7025183$20E48818-8ED2-42C5-B964-12028F60D6F0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0021eb1ef45a5b93ce1d9b7eb620338bc69ad123","datavalue":{"value":{"entity-type":"item","numeric-id":5638281,"id":"Q5638281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$15916547-81F3-42F2-91D0-0321EF9F3C90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b361894c6b71fde79250011881cbf350423ee13","datavalue":{"value":{"entity-type":"item","numeric-id":2996912,"id":"Q2996912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$564B4CEE-7998-4DD8-AD0E-42D91EB366DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61a2286087ed648c5b3380fbb744119aa2e171fb","datavalue":{"value":{"entity-type":"item","numeric-id":2843818,"id":"Q2843818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$1B101370-E55E-4565-A264-170FBD1ED89F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93bcd041174ccd48e10bcb2ce475e4ab10d2f70d","datavalue":{"value":{"entity-type":"item","numeric-id":944367,"id":"Q944367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$4E5C8ECB-E49A-4B55-9D7E-72D854D0A76C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1079b6d698a143d8d07f3dc7f4c3c2ed61bd0760","datavalue":{"value":{"entity-type":"item","numeric-id":5927981,"id":"Q5927981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$C265CB38-9CF1-41E7-93EC-D9D8E55807AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18b28d320f1946e7f3fd48081f2ba560ca397acb","datavalue":{"value":{"entity-type":"item","numeric-id":609451,"id":"Q609451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$A54CDA41-35B5-43C6-B9ED-06F32C7B7FF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a6adc38ea8acb18a1d10ee81a2d3c0baeb25dc2","datavalue":{"value":{"entity-type":"item","numeric-id":2666952,"id":"Q2666952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$909AD70C-EC04-4ACC-B446-8EA56687A98A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5b59558a363f3c3f17ba59b606affa1987e49f7","datavalue":{"value":{"entity-type":"item","numeric-id":1830453,"id":"Q1830453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$63B7FEAD-DB66-461C-9ACA-614873632B07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46faa8f9dd9d2db15375b6f86cd9184a54fb226e","datavalue":{"value":{"entity-type":"item","numeric-id":5505525,"id":"Q5505525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$363705CA-C707-459E-8073-00601D1173AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d48ac30ee5376ad0c91c2b3af2cef2b72d203ef","datavalue":{"value":{"entity-type":"item","numeric-id":5894700,"id":"Q5894700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7025183$CF184444-8B5B-46AF-8D9F-0D3D0FC49362","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Herbrand's theorem in inductive proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Herbrand%27s_theorem_in_inductive_proofs"}}}}}