{"entities":{"Q1006731":{"pageid":1008579,"ns":120,"title":"Item:Q1006731","lastrevid":66566643,"modified":"2026-04-12T10:59:31Z","type":"item","id":"Q1006731","labels":{"en":{"language":"en","value":"Lightweight relevance filtering for machine-generated resolution problems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5532935"}},"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":"Q1006731$5AB486D9-9D6F-4A25-A27F-94B919EB368B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3faf1ab7b3dc171525eac29034dca80256b187bb","datavalue":{"value":{"text":"Lightweight relevance filtering for machine-generated resolution problems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1006731$D04F1E06-3E28-48A4-BD73-F0D136240FCB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"76f921aac0d5bfe80edc5fb1285f94c88144d940","datavalue":{"value":"1183.68560","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006731$EB238D5E-503D-4511-AC29-B7632714368E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"eeec0819ffed3ff77ea39bfc122f96488e0242d8","datavalue":{"value":{"entity-type":"item","numeric-id":1006730,"id":"Q1006730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$EA58D9E4-8F62-46F8-B7FB-199E00C43CF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$C7A22828-753E-4EA8-82F5-B3069550E68C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fd9c858b64e538228c66f00c768fd1506ee71010","datavalue":{"value":{"entity-type":"item","numeric-id":124852,"id":"Q124852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$2F6FF377-34FA-4ED7-A6AE-A9F4CF9BD618","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f17d548f42efb27321ed2d9ca45a732b10fcb2c","datavalue":{"value":{"time":"+2009-03-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1006731$9658C5B8-7E03-43EE-A9E9-AE54EE07206B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006731$0ADD964E-67BF-40A1-B8AE-2D5852CBE299","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a72783658f8c5002247c7fd99e7b67c967c61906","datavalue":{"value":"5532935","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006731$9DC5BB40-13A7-4A92-85B2-22E5F06F3AFF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b21c1d8177ce0f6461c3bbe4e8df47538468468d","datavalue":{"value":"relevance filtering","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006731$24E031A3-7E20-46F0-A314-08736989BDA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eba4308cbe43ddb5eb320cb9e6a534137c293c9f","datavalue":{"value":"proving in large theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006731$6E2ECE45-B22B-4E1F-A66C-E20EE3CDFD0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006731$8F88D1D2-3F17-4F5F-8E9C-4C63B18F6B8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006731$6047199C-4B5F-4148-8314-6D857C85646D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f8701055c53cd72fad85aa7ffb8955b6156a043d","datavalue":{"value":"Q57382620","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006731$C75FB867-B26C-48E7-B3C3-BEE0A4C2F0DC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$90374A23-0020-4594-8E47-9D89C225D91A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$326AA51D-47DF-4504-8A8B-8311E87A012A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$95917695-083C-43B4-9DBB-E85004C6B761","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":"Q1006731$FA0BC70C-0C53-494B-94FB-EE0FDFFA98A3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b8c81b65c08993744b14e4bd26c5542e0a0b660b","datavalue":{"value":"https://doi.org/10.1016/j.jal.2007.07.004","type":"string"},"datatype":"url"},"type":"statement","id":"Q1006731$A7B9C567-71CD-4142-82FA-32F472BC2D76","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5d477ded53dd381ac519b80497cfeb156513703c","datavalue":{"value":"W2013792502","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006731$4E2BA484-ACC4-41BD-95FA-2E02A490A8AE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"efba3487c15800f36ba9934c0e12cbed912934b3","datavalue":{"value":{"entity-type":"item","numeric-id":4524769,"id":"Q4524769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$30054376-D524-4E4B-80FE-462077244181","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b1137cf78c4cad0e217f70ec321f2a593915490","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$20A431F1-C8B0-4F3C-998D-F426E708115A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"388f9bfa40fefe238a0920085d18558ce2b9bc4c","datavalue":{"value":{"entity-type":"item","numeric-id":2492155,"id":"Q2492155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$7CD80652-2F30-42EA-AC5C-BE1BA2B217DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4678e4c2f003554895218494da0c1f6e87bb3ea","datavalue":{"value":{"entity-type":"item","numeric-id":1868508,"id":"Q1868508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$EE3B6D8B-7437-49BD-8A00-C53763FC0746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"785f675ddcdbd72c60ed440a7dd0769c21bb409b","datavalue":{"value":{"entity-type":"item","numeric-id":4263169,"id":"Q4263169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$E4D7B4D8-52FA-4CE9-A41C-A37A09112268","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"216559cea76cbd7bebdc584718098a2b0e882117","datavalue":{"value":{"entity-type":"item","numeric-id":5307074,"id":"Q5307074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$4CA573B8-38EC-437E-9F54-38BE2ABA93D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c00ecccc176b971f8f655f17f279ab75b6423f0b","datavalue":{"value":{"entity-type":"item","numeric-id":2432769,"id":"Q2432769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$89084891-EA4E-45DF-9F4C-13B91ABC83F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5598b9c8536e48580f953ce5c173b0d0770e3a8","datavalue":{"value":{"entity-type":"item","numeric-id":4229404,"id":"Q4229404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$F1BC1CAA-4030-46BA-A1B8-11C28DF66D85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42ba0d7a787c3ddf27f1ee78a59c4dec37184a75","datavalue":{"value":{"entity-type":"item","numeric-id":4520767,"id":"Q4520767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$63614F26-143E-4566-8EF0-A9D93BD3A642","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"040388a79a6c169ddca977411c0445df2cb87a5b","datavalue":{"value":{"entity-type":"item","numeric-id":814429,"id":"Q814429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$F6E9BC5A-718E-4BF6-9CEF-5229606DFBA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ac251759e4b8b56a8b5131e077a39711e974270","datavalue":{"value":{"entity-type":"item","numeric-id":2702602,"id":"Q2702602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$AE4BCB54-CCE3-4657-97BA-A0086E5E2420","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$21610BF5-5073-49D4-B366-C69946822FC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"309a715ecfe3fe3e4ec0e698ae13dce021cfc93e","datavalue":{"value":{"entity-type":"item","numeric-id":2724150,"id":"Q2724150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$AC837BFC-967E-4EA3-ACA2-1A932EE8FA98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$217DF25E-F018-446C-8DFC-C60D34D3A2BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88a75a39f5ac98bf032aaca1eb03b5cd9c31ac38","datavalue":{"value":{"entity-type":"item","numeric-id":5307061,"id":"Q5307061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$56B488CD-58A8-4600-AB1D-D2405C4A5969","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b30f251a9bd5b05c898db8d902209f9dbbeacf5","datavalue":{"value":{"entity-type":"item","numeric-id":4664927,"id":"Q4664927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$9F2734B7-3EA0-49BD-AC2C-A3DDE1FDEFA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bccd1fbbe7b06f5a2e523bc6b279f22309b5dc96","datavalue":{"value":{"entity-type":"item","numeric-id":5307082,"id":"Q5307082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$658B8898-479A-49F8-A529-0E5278A21C9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$C2399D48-3D99-45EF-974A-F418D830A2C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81507f430d90ccca44c5914f167260e0646ee88a","datavalue":{"value":{"entity-type":"item","numeric-id":2751379,"id":"Q2751379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$902A97A1-294B-4FD5-94F4-224FCBD1C738","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47bab4f7d1b2661e9a9ca3ddc35e5a57311ad582","datavalue":{"value":{"entity-type":"item","numeric-id":5507985,"id":"Q5507985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006731$C8665CBB-3FEE-4465-B568-6CADE9375E43","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9ec017c8379c0ee005649dfa3f7e555bc8405af0","datavalue":{"value":"10.1016/J.JAL.2007.07.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006731$B75C1AD2-450B-4C47-AEF9-5B6645DDB072","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a06d00ca5a99ce37bd243a84d6c4d6c10163dca7","datavalue":{"value":{"entity-type":"item","numeric-id":3303274,"id":"Q3303274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5761957c290de5630ea4d00d5984ddec2cdf3b3","datavalue":{"value":{"amount":"+0.7993262","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1006731$0D0A407D-C7F7-4442-9DA9-58981E5E9C49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"054e5fedfc0afea57ed26496b1401118e30c4417","datavalue":{"value":{"entity-type":"item","numeric-id":2077866,"id":"Q2077866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81c7f3b634106168a6edabca2af9f95546f93042","datavalue":{"value":{"amount":"+0.7963687","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1006731$15E69ADD-195A-4E01-8B22-C21BBF9EF8FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fc238813553619fa6517ebfee5a543e5050f8f2","datavalue":{"value":{"entity-type":"item","numeric-id":1587280,"id":"Q1587280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"926126e75d514af37c66164e6f4b7f88234e339a","datavalue":{"value":{"amount":"+0.7709765","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1006731$964E1B5C-96F1-41EC-9656-A78485F3FC84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f8142d06074cc7f600f14ddd4c0f85fbc5c362b","datavalue":{"value":{"entity-type":"item","numeric-id":2568090,"id":"Q2568090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b4d2129e053fc58447ac7566e0ded3bf617eadab","datavalue":{"value":{"amount":"+0.76789284","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1006731$E73EA019-5B56-4AFE-B32F-9503906E27D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dbbf9d404cf9b590634333c1e44728f30862d444","datavalue":{"value":{"entity-type":"item","numeric-id":5318701,"id":"Q5318701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e49a165a2536105837ca2f65fc71300ba02bcfd","datavalue":{"value":{"amount":"+0.766807","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1006731$ABFDE4CE-0651-41E5-B4B6-A8329F4B9401","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Lightweight relevance filtering for machine-generated resolution problems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Lightweight_relevance_filtering_for_machine-generated_resolution_problems"}}}}}