{"entities":{"Q2324203":{"pageid":2334946,"ns":120,"title":"Item:Q2324203","lastrevid":71844405,"modified":"2026-04-14T00:55:02Z","type":"item","id":"Q2324203","labels":{"en":{"language":"en","value":"Unification with abstraction and theory instantiation in saturation-based reasoning"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7105309"}},"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":"Q2324203$7ACD1CA3-537D-4E4D-93D3-E1080A06CF8C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ed540452ccc455db2bd8bdd144960db60bb73f16","datavalue":{"value":{"text":"Unification with abstraction and theory instantiation in saturation-based reasoning","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2324203$AFD21F35-24D9-4208-9EFD-F96757E0CBB5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"540765910f199879446665872c8dd7e048d1ee3d","datavalue":{"value":"1423.68424","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324203$610B319C-4F25-41E9-B737-BB94FE569E8D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e968cb91f72b143c496dd7af71eecd076015c5d3","datavalue":{"value":"10.1007/978-3-319-89960-2_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324203$B6D69E05-99DC-4651-9E5B-AC436434F582","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"395a9171f6bae9b8af4e7440aa83cc44ae6e3948","datavalue":{"value":{"entity-type":"item","numeric-id":2075783,"id":"Q2075783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$73E4F338-C985-4613-8821-8204DC10BC25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5493ce657ff2c3e3dc02ab18ea0d14e2e4a6291d","datavalue":{"value":{"entity-type":"item","numeric-id":748757,"id":"Q748757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$09E4A262-F402-4DE2-89AE-B024C3A6BA86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bab2dfee53655d9cc8087a652185465cb178825e","datavalue":{"value":{"entity-type":"item","numeric-id":229754,"id":"Q229754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$B78ECA78-D2A4-4178-80CE-5052E5326F60","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"96391af82153a94a4af2a0e4c8ac60042cea1674","datavalue":{"value":{"time":"+2019-09-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2324203$6166D1BF-81DB-437A-BBA6-EF4205F646D8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a97c79fc228694ddad6809bb0bfd40beeaa22c48","datavalue":{"value":"https://www.research.manchester.ac.uk/portal/en/publications/unification-with-abstraction-and-theory-instantiation-in-saturationbased-reasoning(13ece419-3c90-4175-8ff8-f6d4a1276e60).html","type":"string"},"datatype":"url"},"type":"statement","id":"Q2324203$064C044A-DAC3-44CF-B952-239A25E7F120","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324203$844AFFB9-9D6F-48DF-BCCB-148C9FF6D65B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e046bc24d7b88fb8ce7108f4a200392d228fc6c5","datavalue":{"value":"7105309","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324203$D6BAB2BC-1B4B-41E0-BB24-6DDBDF268AC2","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$EF010315-9305-42C3-8709-D3014A9F6DEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$AEAC20CB-B20E-4C6D-8444-5607851699C0","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":"Q2324203$AD835A17-CC79-460B-9DAF-90435D3CEF2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$1CC4F934-7F80-4F8B-9F13-499CFB9BBFE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$5E670643-30D9-4EAA-9858-14880969B78D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$308367DB-38CD-486E-AA5D-B9BB409BC0B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5a9d17f73e0a3a248b9a5e7483cd5aefe01a8520","datavalue":{"value":{"entity-type":"item","numeric-id":25563,"id":"Q25563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$38E0E66B-694B-4F5A-A177-E60F1F21D01F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90c7c18880caa813a6bdace0f373d3dec3147690","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324203$66820080-D752-4B57-8870-B06F68F399A2","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":"Q2324203$ECE875AB-514E-4ABC-BED1-829BB7EC99CC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d22e4b9348a9b3873d1a9508dc430018e2341d86","datavalue":{"value":"W2787155581","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324203$3D41B939-4A24-4328-85E9-1303C73539F0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0bd76b240d30f7d32746fbf6c749fe0049139cb4","datavalue":{"value":{"entity-type":"item","numeric-id":2233504,"id":"Q2233504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7d9979bc811b42611cb3a1851a2ea31fb514fbc","datavalue":{"value":{"amount":"+0.7776759266853333","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":"Q2324203$7A8D1784-3525-4200-ABD4-248DDE7599C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a03e5a50c7d4b95055a1ff293851d858aa66aeb6","datavalue":{"value":{"entity-type":"item","numeric-id":5900731,"id":"Q5900731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eaf88e74f57be22788896fa0619fc14478a1a2ac","datavalue":{"value":{"amount":"+0.739761471748352","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":"Q2324203$CED76610-71C1-4A9C-A8EA-B55258A19D0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a163d4150362be8e1e2f5d5bb6dfb8185f2a5266","datavalue":{"value":{"entity-type":"item","numeric-id":5387915,"id":"Q5387915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a7b292d23c1b6b1650c0a3247565330b5aaaa93","datavalue":{"value":{"amount":"+0.7297589182853699","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":"Q2324203$27415B32-3C74-4FBF-A09E-3B6D9DBE561D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"abae2632032a03fe360c1a3290fc2dc2b9b0dcb1","datavalue":{"value":{"entity-type":"item","numeric-id":3541724,"id":"Q3541724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ffa73c635a564b5faf03db6b8136253aac2512fb","datavalue":{"value":{"amount":"+0.7278372645378113","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":"Q2324203$CE99B6A8-C7CE-4A20-96F1-87DCD6CB0108","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"58720908fb6e11f462a0d45eab6a887a79b486a4","datavalue":{"value":{"entity-type":"item","numeric-id":3540073,"id":"Q3540073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bfaf3f4111daeed5413e03f2127e9118b49cff41","datavalue":{"value":{"amount":"+0.7199053764343262","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":"Q2324203$E5E9BFAC-A483-4564-9D63-28958E731969","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Unification with abstraction and theory instantiation in saturation-based reasoning","badges":[]}}}}}