{"entities":{"Q4916079":{"pageid":6945660,"ns":120,"title":"Item:Q4916079","lastrevid":51697604,"modified":"2026-01-19T13:13:40Z","type":"item","id":"Q4916079","labels":{"en":{"language":"en","value":"Narrowing based inductive proof search"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6155891"}},"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":"Q4916079$815C02B1-EBD1-452F-AAA1-80064313A6F7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c38e0916dd658fea30cb1c6645bf23996232c052","datavalue":{"value":{"text":"Narrowing Based Inductive Proof Search","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4916079$887BE0D8-3E46-4A36-8F41-B1BFA4690588","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"26cd3b13f304ec78e2d28861c25185d70817d3c4","datavalue":{"value":"1383.03019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916079$8B41A747-4C3D-4E7D-AD1A-3B0993C73A8D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"382a1c59903156807b2cf8689f9780b507833c46","datavalue":{"value":"10.1007/978-3-642-37651-1_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916079$50F7E3E2-2843-41B3-B60B-89EE68D17C82","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"67de4dcf41337233b478a60d1d06381752453e30","datavalue":{"value":{"entity-type":"item","numeric-id":857912,"id":"Q857912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$B02C0BDC-BC47-481F-84CE-4D1772B28B4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"318dcafa750fdebd097595276bc4d8a687f38a37","datavalue":{"value":{"entity-type":"item","numeric-id":271708,"id":"Q271708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$E694E41D-3CC3-4371-AEDB-37D039C10D6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0d485c18208ab74e19ce1e6fd906e760aa7c6fe8","datavalue":{"value":{"entity-type":"item","numeric-id":1037402,"id":"Q1037402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$6916D884-2E89-4AFC-93C3-0166537F6DDB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3a046867d8df4ef9ef42dfd906417229d4e733e0","datavalue":{"value":{"entity-type":"item","numeric-id":4916068,"id":"Q4916068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$8EE82AE1-2E1B-4C49-85B0-236300AEB173","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"09328fefd4bef3fd48b14da7de769686b3303861","datavalue":{"value":{"time":"+2013-04-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":"Q4916079$0F24093D-A55F-492D-AF77-9C0B0A658EE0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"aca59316c6036425c00d6d140890133ceb7ed2f8","datavalue":{"value":"https://hal.inria.fr/hal-00692193/file/hg2011.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q4916079$2ECF340A-1E6C-464E-A134-3787F86546AF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916079$A1E7B10A-58FB-46B8-B7CE-B54C50BCA561","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916079$096247CA-E757-433B-B9D6-C18D4113C73E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916079$4B85F00E-3E7D-4921-8D78-FFE4B0D9F7BF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3c6daebe886ed0dd73366348dbce43e98652da16","datavalue":{"value":"6155891","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916079$EF2FEBE7-153A-49C7-8A6D-F563DC84A551","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"908a412ea1d66c8c3e12f690543d47d72647ae57","datavalue":{"value":"deduction modulo","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916079$57D218D6-410B-4DB4-A765-7D8A0E791D56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e51a2d9e8f91102f3cb0d41e228201b59d4f55aa","datavalue":{"value":"sequent calculus modulo","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916079$92B48891-F613-49CC-B833-0754BB6609D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa8a6101ff90bea77f851517b5a991ddcaf7286b","datavalue":{"value":"induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916079$8C088342-63CD-4A90-9CA0-192ED19E8108","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"faf1c61e8846e43eb80314c61cfe7f235eec280b","datavalue":{"value":"Noetherian induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916079$098DFEA4-ADB8-4ADA-811C-93DADA8A1A62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9fd4e9fcacc6a19655228c038d1c2ddc3767071","datavalue":{"value":"induction by rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916079$2EC0AFC7-F3B2-48F2-8A82-525D60B97A6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca82b8126faca2bdab3ffa77f0c22600be2e10e6","datavalue":{"value":"equational reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916079$866DAFFD-5CB0-45CD-AD82-F83D006EA583","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916079$7C10462A-456E-4A74-9606-C6482960B3D3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3f1ebf2accc5d6c6b3c7a81ee7493fd53a6bf250","datavalue":{"value":{"entity-type":"item","numeric-id":40618,"id":"Q40618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$916BF459-6909-47F5-9E99-FE0143786E34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4b1f4655c4093a6763ca4d938d08d8f6020262f1","datavalue":{"value":{"entity-type":"item","numeric-id":22153,"id":"Q22153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$A5E9B7AC-6063-4C02-8D7D-01FEC49B99FB","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":"Q4916079$0BF79255-462E-41A6-B918-912021660953","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a951de559db619b11c99eca6c4280e3fcbbff4b0","datavalue":{"value":"W1552653843","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916079$F5726D29-220D-4665-9535-C212E21DAD88","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$92C22D6B-C25A-4DBC-A01A-5B2244A1A8B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db81cf7e79e54426ef60a161c70f4ae06ee9844e","datavalue":{"value":{"entity-type":"item","numeric-id":2942930,"id":"Q2942930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$FD916049-16F9-4E1F-B821-99980DE897E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a42635e354ed5a90dff7abb6b01b6c7ff160dc","datavalue":{"value":{"entity-type":"item","numeric-id":5462949,"id":"Q5462949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$5F68277D-151E-4797-A8B6-55C8768339DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1272332821781f00780d9c30b66a912b70f4d17","datavalue":{"value":{"entity-type":"item","numeric-id":1854350,"id":"Q1854350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$E2D5C14B-2309-4303-A861-0659063CDE10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b37c592ac870d7dec1fc5772fd9a92a63642c5e8","datavalue":{"value":{"entity-type":"item","numeric-id":4808699,"id":"Q4808699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$90425B44-2B52-4811-836E-45759661684C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d087cbdfe7611f0fb92af9e5ed9ae255ff23dbb6","datavalue":{"value":{"entity-type":"item","numeric-id":5900725,"id":"Q5900725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$9207BE00-570B-49C2-A6EF-354AA4BC80AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db15afe119e4d8924199889dafaa491710809a5f","datavalue":{"value":{"entity-type":"item","numeric-id":2751361,"id":"Q2751361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$B4998169-21A1-4232-ADA3-B0048BB89CBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a571653cb6ab1fa29a33b3cbc9d3383816e568e","datavalue":{"value":{"entity-type":"item","numeric-id":2713352,"id":"Q2713352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$63430ACE-B464-4B6C-98A9-D226A86F41F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b714ee7bdb70947b555d42ec2db46670455bb12f","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$6392B20D-7E2C-4F28-BCA9-128D9A6E2005","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$119992C7-EAEF-4467-831C-3D61469D6EDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"682e263c311f9e638f3e45d8e84848cc45a65a83","datavalue":{"value":{"entity-type":"item","numeric-id":1970557,"id":"Q1970557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$BCFB4B14-64DF-4B1D-9C91-ECA441B34F4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab504082e0ddcc1f74e158a854eec65c7cc89476","datavalue":{"value":{"entity-type":"item","numeric-id":1037404,"id":"Q1037404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916079$CCDEDC14-C3E7-4198-856B-19520E743C63","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e6ac4cb02e20675307831c42232123371dc251b","datavalue":{"value":{"entity-type":"item","numeric-id":1037404,"id":"Q1037404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"848d035fcd32763f2f6a1f8b85622e3f8dfd5019","datavalue":{"value":{"amount":"+0.8943538665771484","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":"Q4916079$0E43089D-5828-40FD-B2DD-1C1175767EFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72ce4f9299c3a2986c53414825322ca224e21b8a","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c61cc391557689e9eda5421e072f0e074c658f9","datavalue":{"value":{"amount":"+0.7780511379241943","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":"Q4916079$F07AE771-A066-4D03-8C00-D2A9889F8753","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9a78c41bc3cc611cf5c6ea68d56b3e56736cc44","datavalue":{"value":{"entity-type":"item","numeric-id":4028349,"id":"Q4028349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12ba4c403625a5188939e2a38000de13db5ed940","datavalue":{"value":{"amount":"+0.7669498324394226","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":"Q4916079$DCAF3480-7668-4CF6-A9AE-84BCA6C8A686","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86e48ae2b37dd412c0efbfe692d70a32f72c2b41","datavalue":{"value":{"entity-type":"item","numeric-id":4539606,"id":"Q4539606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cad28592e2e57fa764c26026d5be38679164ef1c","datavalue":{"value":{"amount":"+0.766676127910614","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":"Q4916079$D39A918F-ED99-419A-82C8-5B1F15DA6A2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"620c4caf3dce07d738acb7de2824c5e22e0acace","datavalue":{"value":{"entity-type":"item","numeric-id":5055818,"id":"Q5055818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8fc8e92f41c63e1b7e4ace6fd951849e5479aaba","datavalue":{"value":{"amount":"+0.7626081705093384","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":"Q4916079$F4958C01-5B93-49A5-A8EA-03456235C18D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4916079","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4916079"}}}}}