{"entities":{"Q1334895":{"pageid":1345634,"ns":120,"title":"Item:Q1334895","lastrevid":67432737,"modified":"2026-04-12T17:42:50Z","type":"item","id":"Q1334895","labels":{"en":{"language":"en","value":"Rule-based induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 644670"}},"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":"Q1334895$9BF28EB2-C98D-461B-90E5-C8021BCEAC64","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"46c99028eb87d47e4d0042d705ae9fb3f153c059","datavalue":{"value":{"text":"Rule-based induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1334895$26881440-94AC-49C1-85E8-7A38696EF3A8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2bb9bdb227dfa4634afea3fef48b5788a5db7da8","datavalue":{"value":"0810.68114","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334895$4297F374-E52B-413C-A3DD-9C7537C00C5A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"969e93d58c47e4391e76f2b48bb6ca0c2f0aed23","datavalue":{"value":"10.1007/BF01384232","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334895$B4FA20CB-73A5-4652-A092-EFCEB23090CD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6398cb19c2430ffd14a9abdf2841b97deaf567cb","datavalue":{"value":{"entity-type":"item","numeric-id":1334894,"id":"Q1334894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$04C5B944-4767-416F-80B7-3CA59EFD7BCB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$0DC84384-74C9-4203-A3D1-6BB254F62860","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a07e8af38f76d1e005ebe63136b3f3c24a5ff2b8","datavalue":{"value":{"time":"+1994-09-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":"Q1334895$FAC1989A-F724-4735-8EDB-BB44B45EE7BF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6222e715daa0a9d25b50918db2e2ec31019cbfe6","datavalue":{"value":"Induction is increasingly being mechanized in systems for the formal approach to hardware and software verification. The author presents a method of proof by induction using the expressive power of higher-order logic, as well as the higher order facilities of LAMBDA, an interactive proof system that finds use in the design and verification of digital systems. The system also features functions for the splitting of goals into subgoals, as well as libriaries of common logic definitions and rules. Induction schemes are taken care of rather concisely by rules containing instantiable meta-variables.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1334895$185B0456-F983-4ECA-8676-24DD1D68DCE4","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e860208dea0a8f07f1622b3764a2f40159457c4c","datavalue":{"value":{"entity-type":"item","numeric-id":186051,"id":"Q186051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$9F57F49D-BB69-4585-A6A7-46632F40154F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334895$82B9DFC7-A85F-43E4-B080-B25BCFFE0136","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334895$D348A614-CD51-4411-B978-E5E9D752D5CD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a0cfb2dcf64346a485f5f2b13c8318de162ef131","datavalue":{"value":"644670","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334895$A8C386D0-3B8C-43C4-BC20-CB62CC943E67","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1334895$AC105C77-E833-42EE-9647-F11F6242CB8C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a49c6eab3f20625da110b159712fcc58d765d3c6","datavalue":{"value":{"entity-type":"item","numeric-id":31454,"id":"Q31454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$B3590346-CC17-47CB-AA66-FF7EF8698977","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":"Q1334895$92DA8953-3DD6-446C-B673-5BE2669FB8A8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c91a62fc73d328b39f05fc8fae0c1a2a5426db9a","datavalue":{"value":{"entity-type":"item","numeric-id":685548,"id":"Q685548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$0CA783CB-388C-4C67-9534-9A3942105A95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa81bcc9d031f13e6443e8a60911fc02ec06aa4f","datavalue":{"value":{"entity-type":"item","numeric-id":3992669,"id":"Q3992669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$9BD92C19-4955-4BC7-A986-9F7930C6E91D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de60a74c1ad8598789147a7b11cbf9c8ca77d750","datavalue":{"value":{"entity-type":"item","numeric-id":4028154,"id":"Q4028154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$5A7A3B60-EF95-48F0-BA59-96F9314E555D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$1E6A972F-19D8-4C81-9D3D-2F7C699B2795","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53272d2173db9c6e31a2df5def7f3ca8e8e0c9bb","datavalue":{"value":{"entity-type":"item","numeric-id":3753927,"id":"Q3753927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$9F9044CD-55FC-43A4-A12D-66AAC0918BFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15c8f4c6b02114c3323bed666fcec0afbad9b7c3","datavalue":{"value":{"entity-type":"item","numeric-id":4255517,"id":"Q4255517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334895$23C3AC27-6090-42F1-B816-45FA79CEB944","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95624fd48ac22c1d1a10022afeb19a857a2d7c86","datavalue":{"value":{"entity-type":"item","numeric-id":4712663,"id":"Q4712663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"432e38b57400a56285698b47dbb672a885ccccd0","datavalue":{"value":{"amount":"+0.757849395275116","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":"Q1334895$2E4F1218-6640-4FE0-B4E0-B68D644097B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec40261e8004852901d410e10c4f66c1792c328c","datavalue":{"value":{"entity-type":"item","numeric-id":4849648,"id":"Q4849648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1db818b96c6e3fb2bcb37a6dae4f5cb9c9f06e70","datavalue":{"value":{"amount":"+0.7540431618690491","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":"Q1334895$2BF2D4FD-3EE6-40B3-83F8-518DE037C841","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51852894019aff4da996e23e31ecb38fe929c33b","datavalue":{"value":{"entity-type":"item","numeric-id":2751365,"id":"Q2751365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"027a160cefa032126d3e785c772a8a8231ddfad9","datavalue":{"value":{"amount":"+0.7488933801651001","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":"Q1334895$3F10C2C2-4011-424F-908D-0D586AA22DD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"704a49cab08e72b5b7eb95f34ca27569ea97ba64","datavalue":{"value":{"entity-type":"item","numeric-id":1595923,"id":"Q1595923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"027a160cefa032126d3e785c772a8a8231ddfad9","datavalue":{"value":{"amount":"+0.7488933801651001","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":"Q1334895$AC447D0D-2050-48EE-8695-B2DD732EEABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e81f0140d925efb9c7f35cf9e012c60f913b6247","datavalue":{"value":{"entity-type":"item","numeric-id":4365106,"id":"Q4365106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e2fde9bab9a9c18d6a01396bb3574a61cf57975","datavalue":{"value":{"amount":"+0.7476004958152771","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":"Q1334895$BF2F12E7-B1EE-4E21-88FA-6FDD36072AC4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Rule-based induction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Rule-based_induction"}}}}}