{"entities":{"Q4647498":{"pageid":6677079,"ns":120,"title":"Item:Q4647498","lastrevid":53320880,"modified":"2026-01-24T17:43:32Z","type":"item","id":"Q4647498","labels":{"en":{"language":"en","value":"Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \\(E\\)-unification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001892"}},"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":"Q4647498$C56314A5-3306-4F4B-B244-B703A7538CA4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0444ac259580d9ebae9d1ff67156b5b179333c25","datavalue":{"value":{"text":"Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647498$DF320B51-269F-47EF-AA19-FA6AEDB6B365","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5167594cc10d795e0267488c3a5d67ad88b4e335","datavalue":{"value":"1415.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647498$F703BCF5-641F-467D-8529-98E2B21303B4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c8c475c006c2fcd1a9a0d70c48064524af3891a6","datavalue":{"value":"10.1007/3-540-61511-3_67","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647498$02B0C22C-DE41-4CD5-8D89-2DDFF05EEA99","rank":"normal"}],"P16":[{"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":"Q4647498$578AFE23-1FB2-445D-9127-6763DBF61A53","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":"Q4647498$8BCF20F9-72C2-4BA8-BD29-5084B1214E6D","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":"Q4647498$631A1863-07D2-4CFD-9551-3A162C225FCE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647498$9C311349-F3BC-45FF-A235-42BA1EB06282","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647498$14B6ABE1-E45C-4AE6-A311-D87A520C1261","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5b11bbccd251a5cb930e896125eb7886d52cd403","datavalue":{"value":"7001892","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647498$615CDD21-5642-4AC4-B1C0-18810BDA9C58","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647498$83F38E08-6ED6-458C-92F9-E727C2CA3FEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb3ae69788226feca6ae8044c1c7a9062ebff252","datavalue":{"value":"function symbol","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647498$19BEF9C2-E729-4F1A-BB17-3E75CAD40BDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f3e52067a7ed3ce53605a49bd0992ac3d371713","datavalue":{"value":"inverse method","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647498$6C2C743E-3BD5-45F9-A3E0-B5AFEF172B76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647498$00733198-F62B-45EE-9A2B-03D4F191FAE0","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":"Q4647498$2E1C8F14-B839-443D-BC51-4323AD861EDB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4c1c3aa0c3fd8747f63252a66c59218a9eb25964","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_67","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647498$3271C179-F02E-49A8-AF73-A07DDB8E072A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e1a3a7b39a83ff16a26ff56c63b514790a15ce19","datavalue":{"value":"W1692739636","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647498$2FCB2730-CDA6-4921-BA66-4DDF99C38D66","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bb24ef7f10a33dfe95076d3ff93619b47a1648b","datavalue":{"value":{"entity-type":"item","numeric-id":4113824,"id":"Q4113824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$39181238-1F83-4F18-A314-992911053786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4883090fee4a18fce37441e60e7576f14bdf3e01","datavalue":{"value":{"entity-type":"item","numeric-id":671659,"id":"Q671659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$B05D8518-B9D5-4D2E-B85F-C9949083C7CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dd8d1dd5d31c59ca258af36242eec281a44b582","datavalue":{"value":{"entity-type":"item","numeric-id":3996619,"id":"Q3996619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$6E6FA13E-F48D-429A-AEA2-B7E908A9AC3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"920941013986d0fe98de8d648b55f604839d6693","datavalue":{"value":{"entity-type":"item","numeric-id":4302815,"id":"Q4302815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$A22D460C-626A-4366-8864-457AF7D28CE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"286dba0cbc80cdd0f1ae7c26f1fba8537147aeee","datavalue":{"value":{"entity-type":"item","numeric-id":5620583,"id":"Q5620583"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$2388B503-946A-49F9-97B4-A481DA994DA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$4154A8EE-4A63-4FE5-BC91-1D6AD0631B8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f42400cda0b7b7dd3e21531266007666f2ed8ef0","datavalue":{"value":{"entity-type":"item","numeric-id":5549805,"id":"Q5549805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$2E8CF369-82BA-43E8-B281-4371BADAFE56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$D284D940-6697-4660-94C3-5E61B2529832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb0dd8f8517af3bfb30cb74ae8d68c97c0014f1a","datavalue":{"value":{"entity-type":"item","numeric-id":5581594,"id":"Q5581594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$6C809406-D204-436D-877A-65D030B18AF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f68a38e538d4adda0341dcc68b445865167f58dc","datavalue":{"value":{"entity-type":"item","numeric-id":5551111,"id":"Q5551111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$F9F8CD81-C374-4375-8BCF-36EE71AEC6A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f28e17ba765a588f5157a31e5078c76c4c4b2598","datavalue":{"value":{"entity-type":"item","numeric-id":4109666,"id":"Q4109666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$A717A339-7533-4D1E-A79D-EBBBC48E0818","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1fabe871f96c24655853169e15cfa8cb749690","datavalue":{"value":{"entity-type":"item","numeric-id":1961709,"id":"Q1961709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$62971281-2BAD-41DF-9F44-0DA067D9D723","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$F28C08A2-B4A0-4597-A42A-A736B5CA2FFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febe5bf101c3b7d6dce19439eb466caa5715de79","datavalue":{"value":{"entity-type":"item","numeric-id":5624683,"id":"Q5624683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$E6463CCB-AAF4-4BCA-BCBA-CDCCBEE5A71E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"366403401f7622593b34e9b9dbb671be627d25af","datavalue":{"value":{"entity-type":"item","numeric-id":5285991,"id":"Q5285991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$DF97DD1B-5629-4EC0-91D5-EB836134AE2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4cf7a10bff66d836e836dc6763a8738e552c50f","datavalue":{"value":{"entity-type":"item","numeric-id":4264720,"id":"Q4264720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$703C343D-3AC0-4928-AC95-7BA151C4A07C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8560c579b7bf463389593a93608715865efc3f82","datavalue":{"value":{"entity-type":"item","numeric-id":4647496,"id":"Q4647496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$80E862FC-0094-45CE-8499-4A64459F99A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc1be1343acc1e18378a260b5ef537373326f17c","datavalue":{"value":{"entity-type":"item","numeric-id":4364523,"id":"Q4364523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$456D384D-3F93-4DBA-ADEF-FA5CBCA04FA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db46a24d9e6863a6914bcb7fa90cbe762444f5eb","datavalue":{"value":{"entity-type":"item","numeric-id":4264724,"id":"Q4264724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$5E67242D-5359-44D8-97F0-33D328F777BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54bb8873ce1651399f10a1db5911162e96a0477f","datavalue":{"value":{"entity-type":"item","numeric-id":4645245,"id":"Q4645245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$81EE4FC6-BD6C-4E41-822A-78257A902694","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8fd030717385500bfb13204e49473ce56dd0f9f","datavalue":{"value":{"entity-type":"item","numeric-id":1272615,"id":"Q1272615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647498$567ADBEB-158E-410C-B67C-FDFFD4108A27","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a59ec40c8ef92482d77c211b8284b52f3f1c169","datavalue":{"value":{"entity-type":"item","numeric-id":1810851,"id":"Q1810851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ca8823723578199bd0d107f2208c08fba29af25","datavalue":{"value":{"amount":"+0.9999995827674866","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":"Q4647498$E10C9CFD-88C9-4F16-8CDB-AEB3A4C4A20F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36922c00bbea12382b340d993614db582456c544","datavalue":{"value":{"entity-type":"item","numeric-id":1272615,"id":"Q1272615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0176e4daeff93e8af8780e0240884ab9ad6b07f","datavalue":{"value":{"amount":"+0.94511878490448","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":"Q4647498$A07018C8-1173-4F3A-B908-679921A84CD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da2b6846de4fed4ad457da4792188d08e352b183","datavalue":{"value":{"entity-type":"item","numeric-id":671659,"id":"Q671659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e43ca9332f07079742e9bcea2f9b825e3c3bfba1","datavalue":{"value":{"amount":"+0.8416063785552979","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":"Q4647498$BC6C8C46-FC3B-4B22-AD38-62DEBF0A7B02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca00412e2d39fc69bcc4de993d33880967df5f7a","datavalue":{"value":{"entity-type":"item","numeric-id":4375199,"id":"Q4375199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0d0bfa9050cb6c3fa75fcf2e8837f8e7f67e29c","datavalue":{"value":{"amount":"+0.8279274106025696","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":"Q4647498$EC742DE2-5DB0-417B-B9D7-FA34121D9E97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37e53759432799cbc7db97c1949401fc9d29504f","datavalue":{"value":{"entity-type":"item","numeric-id":4645245,"id":"Q4645245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36f17e428cf13643d0103ee8f4f8ab12531500e6","datavalue":{"value":{"amount":"+0.8279273509979248","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":"Q4647498$A15D0E1B-5C75-4F8A-93BA-7A630A75B516","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647498","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647498"}}}}}