{"entities":{"Q4644611":{"pageid":6674192,"ns":120,"title":"Item:Q4644611","lastrevid":41167606,"modified":"2025-04-18T15:58:41Z","type":"item","id":"Q4644611","labels":{"en":{"language":"en","value":"First-order unification in the PVS proof assistant"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6998045"}},"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":"Q4644611$B83DAE99-3C54-4F64-BB96-9E0C4E7CC28A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b741fec962e8a88d9d2344bbc81d4741a0808955","datavalue":{"value":{"text":"First-order unification in the PVS proof assistant","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4644611$F5D6D60F-2352-4DAB-99F6-3A21D53B6538","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0ffc8415c5a850a59f5015ee8be9266d579a34d1","datavalue":{"value":"1407.68430","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644611$1B3BE221-CE70-4C8B-B521-CFD6182A6989","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"18c300adf8d2a6505f7cd8b2e82685b7b6469055","datavalue":{"value":{"entity-type":"item","numeric-id":2069873,"id":"Q2069873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644611$008EBB15-980A-4F27-AB0E-1FB238CB3149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"baaf8ee5290380abf3ee36f3d116f49dd8b26b4a","datavalue":{"value":{"entity-type":"item","numeric-id":1791142,"id":"Q1791142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644611$C07F279B-E783-496A-9F70-DA4BC1CF4C9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f0a37a82c91a35e36561764c406163ac5986165","datavalue":{"value":{"entity-type":"item","numeric-id":1627456,"id":"Q1627456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644611$75535E27-6FF6-4617-9F24-EAB2465D5595","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb39c66b74dd471ce57c28215b275dfb915aaaa4","datavalue":{"value":{"entity-type":"item","numeric-id":529653,"id":"Q529653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644611$A24C6E46-EC69-48F3-B422-CF0E96EACB11","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"34ad1c5244615701b343bddfc2f0d0c1bd63f8ab","datavalue":{"value":{"time":"+2019-01-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4644611$8D958A69-9AB4-48EC-85AC-2574B7A53C59","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644611$EE7BF4FE-443D-446F-99A4-FCD1614EFD22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644611$172C7C55-6919-48DE-A01B-ED519FA1B64E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3cb2aa05b5b1453813cc3d6d9428ab328e2bd306","datavalue":{"value":"6998045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644611$6E41C531-D697-4B56-9CE6-792C075F0A01","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2b286abd75a54e2934e2a282b76a6708e3af8ab","datavalue":{"value":"specification and formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644611$4C941CB4-5AB7-4551-AD66-2D33D8247463","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d90200d6275680b08dd1574737ccbef35792bd4e","datavalue":{"value":"first-order unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644611$FD2F76AB-0C73-4E11-8212-6813F2938627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06532801be3fd5adcac631b84b2774288d527d0b","datavalue":{"value":"existence of first-order unifiers","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644611$2820C8BD-2B67-4891-BBA0-D967E92E8118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"185326cd89c8536742bf52a6007685b103bd0f6a","datavalue":{"value":"verification and correction of algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644611$7FD8E44B-59E0-4BB1-A7C1-765770712266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644611$7071AEE9-B362-417B-B91E-1A87EB2AC3AE","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":"Q4644611$0FE06305-2C7D-4984-A531-37EE310D7024","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"07f0f95931fd7b98915704b51034dfb3bde910cf","datavalue":{"value":"https://doi.org/10.1093/jigpal/jzu012","type":"string"},"datatype":"url"},"type":"statement","id":"Q4644611$24E94956-D1B9-4D05-8025-014568DF45C6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"991a70346dcba78db904df7110934d8cf25764be","datavalue":{"value":"W1973876376","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644611$DD056854-8836-4174-91DD-6D9C828D7E78","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"9bfbfc243cfa9a23dc1aa5e3b4cf61b037f68093","datavalue":{"value":"Q58001385","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644611$C8AFD655-8069-4D46-AC40-7DDB54913649","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"714c6169066405f69a3c9f77a594479a9e603027","datavalue":{"value":"10.1093/JIGPAL/JZU012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644611$28321EF8-D0F2-4AC7-AEBC-9314BE202FF7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2322a21df36f02b2b9c16a6174c764d5fc949009","datavalue":{"value":{"entity-type":"item","numeric-id":3061274,"id":"Q3061274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644611$9B701998-A4FC-41DF-925A-BE4F69263947","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1be56a5e540eb2a386bedc5e403d6cf01ab17e69","datavalue":{"value":{"entity-type":"item","numeric-id":3160301,"id":"Q3160301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6567f762d4155030813c5c1b52e7aa13e08d9c68","datavalue":{"value":{"amount":"+0.86568135","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":"Q4644611$334D5D94-8CE6-4242-841F-6E9F270AB15F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddcd94f921aa20f6b9b45b22d22d4796be094a6d","datavalue":{"value":{"entity-type":"item","numeric-id":429582,"id":"Q429582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f84dd71ffdc7e2f036c3733dfdb090c49a6e55c0","datavalue":{"value":{"amount":"+0.8650553","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":"Q4644611$6B99E266-D3A2-4C35-B4C7-9221729B7D84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fca0e7e93dd7042cbc7e59c47a83bea11c5a6406","datavalue":{"value":{"entity-type":"item","numeric-id":3612467,"id":"Q3612467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e99155463fa6688d857828f118ea5b0089d426db","datavalue":{"value":{"amount":"+0.86012787","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":"Q4644611$0FB7B1C5-3862-440A-82D3-7ABE54CB8722","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d582558383118de9d65b0211933a9afadc6cadfa","datavalue":{"value":{"entity-type":"item","numeric-id":4357064,"id":"Q4357064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d48159a5d886ca9f7d19491c878e8d8407550c99","datavalue":{"value":{"amount":"+0.8599378","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":"Q4644611$825598F3-50D9-4A63-A265-B18043B65BCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9765cac59eddcea60234504b856d9327e06abad7","datavalue":{"value":{"entity-type":"item","numeric-id":3496309,"id":"Q3496309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2211d937eeaac88e4a24d951e1331d1350ea961","datavalue":{"value":{"amount":"+0.85885143","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":"Q4644611$89D2DFDE-E8B8-4F04-BB69-39349A29F666","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b39468ec26c8b1fe3fe504815fffeb4b9bdd04ca","datavalue":{"value":{"entity-type":"item","numeric-id":4703041,"id":"Q4703041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1aa5b19fe0e34f174637005bf0f91a17035244c","datavalue":{"value":{"amount":"+0.85821414","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":"Q4644611$37EFBD18-4764-491C-A113-1DFA0C558D9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"998e4a8effba2b1878cb890fe472349cb9616c3c","datavalue":{"value":{"entity-type":"item","numeric-id":5858677,"id":"Q5858677"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"83d4a631c5a47e367a59e1180257061b4ed3752a","datavalue":{"value":{"amount":"+0.8536844","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":"Q4644611$0018AAA2-2F1D-4A09-96DB-2D3B32A87C1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc245bcfa199f7a5de18df583433563380e6355e","datavalue":{"value":{"entity-type":"item","numeric-id":5307478,"id":"Q5307478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e245406127ae0ee5ead3307a84d63e421de4d475","datavalue":{"value":{"amount":"+0.853088","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":"Q4644611$97869DA2-7E1E-4C6D-9584-C6C393D28672","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4644611","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4644611"}}}}}