{"entities":{"Q2491080":{"pageid":2501823,"ns":120,"title":"Item:Q2491080","lastrevid":73484814,"modified":"2026-04-14T16:10:36Z","type":"item","id":"Q2491080","labels":{"en":{"language":"en","value":"Herbrand's theorem and term induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5027255"}},"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":"Q2491080$20082396-A2D1-47CA-BBB5-A5B1D2927027","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e409ad343037dd1767bbfb486f29011e3f191a30","datavalue":{"value":{"text":"Herbrand's theorem and term induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2491080$88917631-4C62-4312-AAE0-4A66468147A6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ea1a4bb00365f1c3b18a6eebbc562b57f2928974","datavalue":{"value":"1093.03032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$BF927B42-7C9D-4922-82D6-9722B9A2B0FF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ec91c84374e1970ffeb850b5b07163b4a998968b","datavalue":{"value":{"entity-type":"item","numeric-id":167059,"id":"Q167059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$8CC6711B-2CE3-416D-A442-902FD8BBA351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"72dabc59d6ac55abae8a5d41136834dd0407ff86","datavalue":{"value":{"entity-type":"item","numeric-id":276250,"id":"Q276250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$E92978E7-D6C0-4097-BBDF-2BF2CC2A60C9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$0CAFC7FC-66F5-4618-ADD3-B847754BF711","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c4c8103b3de3619e9a7a179137854980af704334","datavalue":{"value":{"time":"+2006-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2491080$47262220-59A6-4C37-A38A-26EAA8152E2F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4560ff03e477b21ddd88082323de34842f6a939c","datavalue":{"value":"The authors consider a cut-free proof system TIND, an extension of Gentzen's LK by the following purely logical inference rule of term-induction  \\[  \\frac{A(c),\\Gamma\\vdash\\Delta,A(S(c))}{A(0),\\Gamma\\vdash\\Delta,A(S^n(c))}  \\]  where \\(A\\) is quantifier-free and \\(c\\) an eigenvariable. This (tind-)rule, formalizing a restricted induction principle and deriving numerals instead of arbitrary terms, can be considered a logical image of full induction. The context of system TIND makes it possible to study a reversion of Herbrand's theorem. In fact, a generalized Herbrand's theorem for TIND is proved: if an existential formula \\(A\\) is provable in TIND, then there exists a Herbrand disjunction \\(H\\) in matrix form such that (a) the length of the corresponding matrix is uniformly bounded by a primitive recursive function depending on the length of the proof of \\(A\\) and logical complexity of \\(A\\), (b) the number of `big' disjunctions is uniformly bounded by a primitive recursive function depending on the maximal iteration of (tind)-rules in the proof of \\(A\\) and logical complexity of \\(A\\), and (c) the term-complexity of the reduct of \\(H\\) is uniformly bounded by a primitive recursive function depending on the length of the proof and the size of the reduct of \\(A\\). Consequently, Herbrand disjunctions in matrix form are conceived as natural characterization of theorems of TIND.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2491080$9F661958-F195-4C53-B5C3-8B87886D0B0A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$E5F60A9D-4DD7-44B2-839C-D727E954294F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$B0C100D8-009A-432F-879F-9CA014877CA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$692DCDB5-03C0-454D-8F85-6AB1A19A3E3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$B7334AE3-E948-43EB-BE56-3E774CA55A37","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"819caadcd377a569e5745bfe7a4d52f0eecfbb0f","datavalue":{"value":"5027255","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$195F8F93-3F11-4B5A-B21A-C97586D92009","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a09c1984b41935c0a923dca51c0af0797d5eb50a","datavalue":{"value":"Herbrand's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2491080$6C3E08E2-B752-4413-8DE0-4F326CF2728F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05d96f7c660a89f9449a72ca84fc6fa97ab47d9d","datavalue":{"value":"term induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2491080$5EC32B8F-5583-45D6-8500-D3AA870EAB58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d170b16db9de34471796f51d060242d2febb5b51","datavalue":{"value":"cut-free proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2491080$704A002A-DA80-45F8-AF1E-3BE033C13F52","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2b87c2901b1d9462aa6fffa26502c8ee861836b0","datavalue":{"value":{"entity-type":"item","numeric-id":1062052,"id":"Q1062052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$D8AD552D-870F-4A0C-9A9A-D36260FD7782","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$03748999-DFF3-463B-A796-2DDFAD0C09E6","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":"Q2491080$F6262000-9C1C-40F1-85BA-DB9B1605D825","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"62c38f45d56fc83a2d1d90f72582e840d073d907","datavalue":{"value":"https://doi.org/10.1007/s00153-005-0327-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q2491080$F16B250D-EA04-4CA0-90DF-671FC50D4E63","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0f3ca3081eb62df82ee10e3cf4da2cc63894f7aa","datavalue":{"value":"W2009766573","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$18DF45B0-D190-4E0A-B54B-037A6BF2BE63","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a351897245977aa0d098a2219b09f6d20cfa230","datavalue":{"value":{"entity-type":"item","numeric-id":2751360,"id":"Q2751360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$CC86C84D-E734-4FA8-B519-B66727F8A678","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"805ffaf6ed1ac838a4cdfd27c2248369dc7c8fa7","datavalue":{"value":{"entity-type":"item","numeric-id":3469102,"id":"Q3469102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$97DB6ED0-6C21-41D6-9D67-CBFEE35725D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ac913c59bc63f798e3256ace7ff41f5e40f7db5","datavalue":{"value":{"entity-type":"item","numeric-id":4436025,"id":"Q4436025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$2D494FEC-2A3C-4639-8237-86E9C93AD286","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":"Q2491080$96535C1E-3688-4B08-8A4C-BE357229B9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0508654f8dbc2c54065d5adc87d2e81f95024db","datavalue":{"value":{"entity-type":"item","numeric-id":1302302,"id":"Q1302302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$FDF4FB43-186B-4BE6-AB6E-586F8C0664C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac25e63d54594f5eb2c84da7217cf5a703f75a44","datavalue":{"value":{"entity-type":"item","numeric-id":930260,"id":"Q930260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$D3A90202-0A37-435E-BF14-1A0419DF3288","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b50569bab229d364cd322407418c533adee44dc5","datavalue":{"value":{"entity-type":"item","numeric-id":1899140,"id":"Q1899140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$E6990319-4562-474B-8F07-4CEDAA95C0A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af4555c0d89e243a8a9351cedc1b4ffbfceace09","datavalue":{"value":{"entity-type":"item","numeric-id":5691140,"id":"Q5691140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$2D503846-7934-4999-AECC-7EDFA95F21F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$2B97D687-B2F3-4750-8CC4-5B3F201246BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"635d658e492778c40a0dc6463613126938b64c17","datavalue":{"value":{"entity-type":"item","numeric-id":2751365,"id":"Q2751365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$B7E23971-A4B3-4147-A6F0-065AB5B190D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2ea905e0dd45e5f666435e07c5347d2d8ec010b","datavalue":{"value":{"entity-type":"item","numeric-id":4215630,"id":"Q4215630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$25CD6E4C-FE51-4315-949E-E37596D56ACB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$918A344E-BD89-4239-B005-D24E6A3CB0A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77351dbabf5bebdfbc98823dc61ee4a06c4f1b6d","datavalue":{"value":{"entity-type":"item","numeric-id":5625113,"id":"Q5625113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$AD975612-ACC5-4B31-AC42-13FF672B7A9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e1a301cd93c8014a1841e85fdb1644154a042ba","datavalue":{"value":{"entity-type":"item","numeric-id":5611757,"id":"Q5611757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$97667415-7DCA-46FF-9E59-FFF8B1C64C40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b880d3c8511f1d53c27d1537b521daf74193b4","datavalue":{"value":{"entity-type":"item","numeric-id":1102280,"id":"Q1102280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$F95F552B-E6E7-4F83-89C7-CF8F228107B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f70c7f0070211df81086d4c25b73a9ca61d45c1","datavalue":{"value":{"entity-type":"item","numeric-id":5686023,"id":"Q5686023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$C4DBC6C7-3D0E-4C1E-8A7A-1F5848CBC0A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e499c86ee0646fff12cf3f079c9131faaea7b20","datavalue":{"value":{"entity-type":"item","numeric-id":4215637,"id":"Q4215637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$E35CA72E-A20F-4DBC-B1AD-9B852CCC9616","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1b4998bdaf1a6b4855ad6d2b807b069f618a518","datavalue":{"value":{"entity-type":"item","numeric-id":4041554,"id":"Q4041554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$7EBACBC2-972D-408A-9CD2-C71C0F837BA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7c3e6815cd921fc7767de9db6783bde242a686c","datavalue":{"value":{"entity-type":"item","numeric-id":4143279,"id":"Q4143279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$FCBFCD5A-6AE7-473E-A537-DF28B40E1BEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01f3c9efa192a49157794cc5646843be5e89451","datavalue":{"value":{"entity-type":"item","numeric-id":1086559,"id":"Q1086559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$162DD33D-6D57-441F-AF2B-34545E5D981A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c07be1bb84c31825342615f567467fa862f8d1e","datavalue":{"value":{"entity-type":"item","numeric-id":4299360,"id":"Q4299360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$B748E303-43DD-49CA-9129-308A5660441E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa011a834041a527ecea97cb500c12560c9ab895","datavalue":{"value":{"entity-type":"item","numeric-id":3335776,"id":"Q3335776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2491080$E7D04205-F286-44C5-853C-7CFD8288A13F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5414be8d194990098d7e20c6ab7bf2b83e55b772","datavalue":{"value":"10.1007/S00153-005-0327-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2491080$80F9273B-E2AF-4C50-96EA-8DE73ACCDBEE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"927de2036c04d73625e0d30f14439bf2d3b81a74","datavalue":{"value":{"entity-type":"item","numeric-id":4783326,"id":"Q4783326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9829d3ce6d36775596b69a75a86cc873f8262979","datavalue":{"value":{"amount":"+0.8169345855712891","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":"Q2491080$8CB8B7A4-58E3-4E25-AFDE-7570974388E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bb712603a97d95c8c6f1736d1041e8ebba15328","datavalue":{"value":{"entity-type":"item","numeric-id":1709711,"id":"Q1709711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bbfb5840f69785feeb2099830f2a6f7258a7440","datavalue":{"value":{"amount":"+0.7086020112037659","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":"Q2491080$C5469FA7-8245-4D33-9080-57C309E143F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95330b6380a0d5189187a11071d582fd9182a70a","datavalue":{"value":{"entity-type":"item","numeric-id":2502163,"id":"Q2502163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6746d833738dd2b8138950a34e2242740172d8e","datavalue":{"value":{"amount":"+0.7068538069725037","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":"Q2491080$4CD27BC8-65A0-4FD5-BB4B-F0A90F546B53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae6a11fe9c7925bce8eaf884ea4961802e808d16","datavalue":{"value":{"entity-type":"item","numeric-id":2751366,"id":"Q2751366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d80951a2a888122c78ac6db666abdd2236b305a3","datavalue":{"value":{"amount":"+0.7018483281135559","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":"Q2491080$13DE9743-606D-44AE-A382-D4673029EB8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1590ce945709859e583973741e1267839f8cd55b","datavalue":{"value":{"entity-type":"item","numeric-id":2486989,"id":"Q2486989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d80951a2a888122c78ac6db666abdd2236b305a3","datavalue":{"value":{"amount":"+0.7018483281135559","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":"Q2491080$CCBBD2A0-3440-42FA-AAEE-E407168891E9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Herbrand's theorem and term induction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Herbrand%27s_theorem_and_term_induction"}}}}}