{"entities":{"Q1148892":{"pageid":1159641,"ns":120,"title":"Item:Q1148892","lastrevid":42912526,"modified":"2025-07-15T23:27:56Z","type":"item","id":"Q1148892","labels":{"en":{"language":"en","value":"Using sophisticated models in resolution theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3708347"}},"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":"Q1148892$092DA26B-A848-40F2-8281-37B3DDECE01F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b059638e2b210efd6da26b59c581dc54c6d18708","datavalue":{"value":{"text":"Using sophisticated models in resolution theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1148892$5E28D17D-4700-4AD4-A149-8785A16805DE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9f4839ef5ab3ce6a5939eadc0404a6ef425d763f","datavalue":{"value":"0453.03014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1148892$8570A09A-197C-4076-8BF3-C8C22918EF3B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"74e7c88adecbaf1a4f7212a1095797371ba5ceb0","datavalue":{"value":{"entity-type":"item","numeric-id":1148891,"id":"Q1148891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1148892$7476AD4F-4854-44C7-B0C4-2981EEAD649A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1148892$275AB057-C1C3-4E12-8B4A-6C58B0F4EF69","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"56afe75e154439409929c71e0e459d1542811b6e","datavalue":{"value":{"time":"+1980-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1148892$FE5F11F3-EA5A-487E-A65F-ACD6FC94FE65","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1148892$C9B373C6-7EF5-417A-A969-3CBFF27B98DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"89663cdc2c9f64b2cd0a104bcac86329d89b9b2d","datavalue":{"value":"03-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1148892$90C8EB27-CAFA-414D-93E9-9BF09FF89935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1148892$DF001F15-5A3F-4C6E-9913-08E0A3DBDF5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1148892$4D4F0337-00E1-4976-B867-4FDC6961A0CA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9e84878e7d7785b4a09dfdb8998a7d894d3ac6d8","datavalue":{"value":"3708347","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1148892$BC16F568-2FC5-455C-ADD8-2D14E75238A5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03158307b01a6e2de96f5585d7a65d8e1a522aae","datavalue":{"value":"resolution theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1148892$6C5A8DFA-5C6F-41C6-A889-FB3F24C21149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9a33bfb266517f37c2893982b2b0f9fde5f7330a","datavalue":{"value":"models","type":"string"},"datatype":"string"},"type":"statement","id":"Q1148892$8C019984-1F34-434E-BDCB-3FDBC4D04713","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6444bfd6c253e1dd7ebe9e0d3bc7dc84255fa98","datavalue":{"value":"semantic functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1148892$36BFF757-35E5-47C4-A4FB-E40AE789482B","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":"Q1148892$434742CE-7E16-4CC0-BD2C-68E3FF8AEB4A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1148892","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1148892"}}}}}