{"entities":{"Q4647502":{"pageid":6677083,"ns":120,"title":"Item:Q4647502","lastrevid":53320889,"modified":"2026-01-24T17:43:33Z","type":"item","id":"Q4647502","labels":{"en":{"language":"en","value":"Internal analogy in theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001896"}},"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":"Q4647502$4AA9172B-A2C2-4A26-B66D-3F47EEB09074","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"52f013f20fea6fec9f971612b425f90382d0c834","datavalue":{"value":{"text":"Internal analogy in theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647502$95E3B254-90AE-4172-B68B-A8A8924AB640","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b3c281308a571783e2fa0a08c5e474fba9b97234","datavalue":{"value":"1412.68245","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647502$9DB8F0CD-C9FF-4C70-8E59-3DC22663AAA3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"92ec180fd12c3b93d94950f84417445b37a19e99","datavalue":{"value":"10.1007/3-540-61511-3_71","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647502$6198C32F-CE12-4A38-9ABF-8DFF4B4336B7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9b7b87520b581501a7aa2502f13216a81e8bccee","datavalue":{"value":{"entity-type":"item","numeric-id":699919,"id":"Q699919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$422476B6-9AEA-4F62-B92B-3E7A0228A8C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8277b97ee89f3f6e73af930a736006548fe36efb","datavalue":{"value":{"entity-type":"item","numeric-id":1188507,"id":"Q1188507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$EEDE3128-9C2F-4FF5-8D55-20652706761C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$B5BD8EA5-13C3-4CF3-AF0B-C892E52F2CF5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647502$D87C2380-DE10-45C8-B3ED-021C6418D518","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647502$62D1C4A7-1856-4A3A-9858-9582901E27AE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7616c52d320502f213f722b1668dfe5edfff8a61","datavalue":{"value":"7001896","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647502$7E068D77-5CA3-4C4C-B28E-D7A72CA33081","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8411e18cef6b59c69a917056bf1d60b65a4f9161","datavalue":{"value":"wave front","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647502$87160FE2-3D1A-413D-B944-162EE74A8C69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647502$8FC456F2-9EB8-4632-B152-72100BC0C091","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbcb7fcc1cc590b688dad6087563f1ba17c06258","datavalue":{"value":"critic application","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647502$0DB61CE3-ABF0-498D-986A-2180CD3108D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c40a6b182efd93977e2c635a63b760f3bfc2c9b","datavalue":{"value":"induction scheme","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647502$DB800E00-1848-44D4-8DA1-A20F370F836E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70b50395265d888951b313aa43e4197639396288","datavalue":{"value":"current goal","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647502$73E46AF1-1A7D-45B9-953B-86AED98EAEFB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$4CDFE90F-0CF9-439A-9651-01547B8C8D78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f10e7acb77aa2a053602f0044c4781346f0cbb55","datavalue":{"value":{"entity-type":"item","numeric-id":31444,"id":"Q31444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$5B5834A5-21FC-4866-993B-B8F17867009D","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":"Q4647502$ABA3292D-3341-4A75-BE23-9A60B484EEDC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2765ded8e3ebc5e56af6140d79b8b370620dd97d","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_71","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647502$0A94F07C-1326-4D40-8974-03A1237DB4AB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"94c1ed28c6b990d1806ae931278e3eccedfa5e19","datavalue":{"value":"W1490982973","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647502$729D6EEB-3F8B-4F2E-9BC0-142434576B8A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f5ae27268a48b91a2cb9712e13b2ccff954f2260","datavalue":{"value":{"entity-type":"item","numeric-id":809617,"id":"Q809617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$7AFFB284-7842-4BDA-A445-F0281CC0C9E8","rank":"normal"},{"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":"Q4647502$00FA7D14-D67E-4FB3-9973-4C654127911D","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":"Q4647502$7BE08700-DCA4-4AA9-8E6E-48AB3AF9DA58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7db98659fd0d8d989353341e0c12c4246dfe6ee1","datavalue":{"value":{"entity-type":"item","numeric-id":1915134,"id":"Q1915134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$0023C243-1A42-4667-A94A-7640D8D87F4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bab9ab22080967e5d288bfe71ea650ed7efe6f4e","datavalue":{"value":{"entity-type":"item","numeric-id":4002491,"id":"Q4002491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$A94BFDD6-A6DE-4CD1-9B11-5F62875648AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a0bfd492dc5440205bb23db5301e8568f83f4cc","datavalue":{"value":{"entity-type":"item","numeric-id":1419888,"id":"Q1419888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$B667E943-ECE2-442A-B5D6-8F6FA2FF0783","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5230907bea404aa6c2fb79168521e88708f2a2ec","datavalue":{"value":{"entity-type":"item","numeric-id":6488528,"id":"Q6488528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647502$E570AAD4-673E-46A4-8CBD-D527DA92D38D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"31ef04229fe5b87a8f06fd4e0326e4847ef09985","datavalue":{"value":{"entity-type":"item","numeric-id":1283199,"id":"Q1283199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff64306c5d74e45d57978daf28ebae3812d1c0bd","datavalue":{"value":{"amount":"+0.8330597877502441","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":"Q4647502$0567A9A2-60E4-46EE-974F-D061AF46B610","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af8daebb386f5b0811f7c17763d9beb7f6aeb15c","datavalue":{"value":{"entity-type":"item","numeric-id":5234724,"id":"Q5234724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3cc21c36da1feb7a84fb2153f4096837bd482c75","datavalue":{"value":{"amount":"+0.7341752052307129","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":"Q4647502$5D1C5BD0-BAA8-4F00-A1F2-07C7F889DD5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a5348b8a4e161aacdbed50cbbc41d026a283965","datavalue":{"value":{"entity-type":"item","numeric-id":3817655,"id":"Q3817655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce07bc035d4988561c4d56fa3633b5fc3d44afca","datavalue":{"value":{"amount":"+0.7261400818824768","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":"Q4647502$E4EFBD99-F570-4847-9637-E4C222294ABA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7334020c30173115a8fb2673f1d4e7ebbc6d3d21","datavalue":{"value":{"entity-type":"item","numeric-id":5235252,"id":"Q5235252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b264f413e6216965cc343a2bebf2703033d02bf0","datavalue":{"value":{"amount":"+0.7179961800575256","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":"Q4647502$737B9A7C-CB65-4B3B-A6C4-81FAEA3E4E22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20a666456026cbeb2b2c1988334a1396c6b0dd8d","datavalue":{"value":{"entity-type":"item","numeric-id":5739522,"id":"Q5739522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee6cd95e0f1a0dfe35ead6c3a9b7c7dd89bf463d","datavalue":{"value":{"amount":"+0.7127389907836914","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":"Q4647502$D56A9908-7DDC-4A61-BFDD-F067BE7E95AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647502","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647502"}}}}}