{"entities":{"Q6893591":{"pageid":20858074,"ns":120,"title":"Item:Q6893591","lastrevid":84191153,"modified":"2026-05-13T09:59:27Z","type":"item","id":"Q6893591","labels":{"en":{"language":"en","value":"Theorem proving as constraint solving for coherent logic with function symbols"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8128172"}},"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":"Q6893591$A2A09A95-34BB-449F-AC78-46087AB605E4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c622f6c30aedd1addd3968d57c3f2933d7ce8dac","datavalue":{"value":{"text":"Theorem proving as constraint solving for coherent logic with function symbols","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6893591$3095FBF2-18C3-406E-8140-FA4C1F4DFC14","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"192d6d0e173404e703e6c07df2c6c059d15ceeb0","datavalue":{"value":"10.1007/S10817-025-09742-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6893591$57211579-2C6D-4380-934B-7EF9DA35E1C2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c93dc7f088015e9cd1eacb5d2c04306baf043d99","datavalue":{"value":{"entity-type":"item","numeric-id":286775,"id":"Q286775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$C7564C26-5307-4045-9795-B1949A9EF25B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$26F1D9F4-6516-49F9-B34C-ADCF4632730F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"46b64429f4db778a47f40be8c6fa42e140125f60","datavalue":{"value":{"time":"+2025-11-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6893591$F4BEDF1C-9213-4971-AEE3-D25E98D1C279","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6893591$202624C7-E765-472D-8130-4A65D73830C0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5182ccdfa821ea06ea7a0c31db4b9b1d355fbabf","datavalue":{"value":"8128172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6893591$953BC3B8-91FC-4E08-84FF-46A8902BCD57","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"223556ef87b8f25f218d19756cbdf5e24d0a2719","datavalue":{"value":"coherent logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6893591$3FC766CB-1516-44C0-9347-9614DF91B8C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6893591$5387C7EA-305C-4CE1-AE8E-4D1A14AEFBEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b97591a1eec270d79d6d5074b2e7530729653abc","datavalue":{"value":"readable proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q6893591$60AD32A1-4F7F-491C-8ACE-27E4FE3F8156","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"89d37044de50fffb430d2b2cd96ae173eb26ab87","datavalue":{"value":"verifiable proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q6893591$E19E73D6-DCE0-4A1D-8812-E2CD464FA715","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2440c6394e2ac24533843222855bcea18333dee","datavalue":{"value":"constraint solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6893591$C2090C2E-485D-4318-B822-4632A5D2C3FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a1509357c65c35f25ca4a3489812a49ab4a22a9e","datavalue":{"value":"abduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6893591$8A7770C0-0750-4A93-8722-F5B6B8A638BD","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":"Q6893591$238B885B-05FE-4EEB-A976-1771E06CF2E9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"05d29c3caad4ac794c62be84521ad055da0d81da","datavalue":{"value":{"entity-type":"item","numeric-id":850998,"id":"Q850998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$AB0E83E3-9558-4A9A-9F09-A82365DFA937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5552c73af9ffa4d08773105bfa675feb6642eb2e","datavalue":{"value":{"entity-type":"item","numeric-id":3453119,"id":"Q3453119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$97F36F20-6422-4006-8851-15A9ACD5F541","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed1b64e7e3e0a9250bcf98bbe7b0e8298f79b9f5","datavalue":{"value":{"entity-type":"item","numeric-id":7025230,"id":"Q7025230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$52C2B5C7-89A5-444D-A722-DF046E4C505A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6820d466f20a132975882100c6125897eef0f140","datavalue":{"value":{"entity-type":"item","numeric-id":5309032,"id":"Q5309032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$A578BC94-CCB8-4E9B-A596-3912DFB74D92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"686d8c1af79a48830313f258a972641c870a4f2f","datavalue":{"value":{"entity-type":"item","numeric-id":2631965,"id":"Q2631965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$1771874C-64F9-46FB-BCCB-84D76BC11244","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$5B5BA902-438D-454E-8EEE-A3BE35DA8AC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f387953725247a87a3205c679d46a0a2c63b7e5","datavalue":{"value":{"entity-type":"item","numeric-id":5898147,"id":"Q5898147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$2B4A3359-F011-4829-A0E9-CE3D9C55C6F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b9f30a506579d570709211d696ed5ba11d9cc6f","datavalue":{"value":{"entity-type":"item","numeric-id":4665735,"id":"Q4665735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$94A289B3-EC92-4762-BF0F-84456DA2AA75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30492f77eb016746469a740ef03c349aed405ecd","datavalue":{"value":{"entity-type":"item","numeric-id":5387843,"id":"Q5387843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$CEE6F0F1-21E0-466E-B089-2AE4D30FD5A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5791688c0d08cb0956d2f1e861eee0a36c47d237","datavalue":{"value":{"entity-type":"item","numeric-id":2471743,"id":"Q2471743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$EEAA2245-A90D-4781-81C6-2124AA61A063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42e95031f926c5f0524c20cbbb322383964510ed","datavalue":{"value":{"entity-type":"item","numeric-id":2864408,"id":"Q2864408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$C118D4CC-7815-4114-885F-400B5AF243EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d45ba0f08d8b9ad108013eb53fd86281684a152c","datavalue":{"value":{"entity-type":"item","numeric-id":2849509,"id":"Q2849509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$DF011DE3-13F9-4F6B-A2EB-8FD2EAACE9F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"981b322b800f12891beed18d9218a5203bf47bb6","datavalue":{"value":{"entity-type":"item","numeric-id":2351156,"id":"Q2351156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$C3C8BDC3-C87C-4C79-9DC9-F4BF4CBBF4C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de66456d0982b9e07ca51cdf5d084090ac8dea2e","datavalue":{"value":{"entity-type":"item","numeric-id":2104525,"id":"Q2104525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$31046DB3-198A-44B0-A285-6505BCDEB753","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15969da430dd79b9be0499621aa8cddedb6a17a1","datavalue":{"value":{"entity-type":"item","numeric-id":4935259,"id":"Q4935259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$BF1F3026-C55C-4DCB-9213-E0B4749C6F6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f28586038cea8cbc7416baeda543b4e3023f378","datavalue":{"value":{"entity-type":"item","numeric-id":4707746,"id":"Q4707746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$912F3490-7BC0-4034-81F5-8F58D39F9986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b547ecbdee111d500340a1755c27397d76f7d718","datavalue":{"value":{"entity-type":"item","numeric-id":3608794,"id":"Q3608794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$923DFD99-03A1-4890-B5BA-C6838821C32B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a08243fd980f5701ca2fc53c5c48bfcfef4aa6d","datavalue":{"value":{"entity-type":"item","numeric-id":2795295,"id":"Q2795295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$52599A50-47B1-4745-8810-A088028D132B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f660261386a269c5c6d007e1774c790f4ddf72ec","datavalue":{"value":{"entity-type":"item","numeric-id":5815602,"id":"Q5815602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$B17451DE-C6BF-4674-B046-B455CC47A0CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"456f56a3bc1b171a4303d760aadc2dfb87f35efa","datavalue":{"value":{"entity-type":"item","numeric-id":3166220,"id":"Q3166220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$42E464C1-6BAF-49CA-9E97-39D352E388F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bf26db92fe44f4617dcc2f7627ea50e8798a1d8","datavalue":{"value":{"entity-type":"item","numeric-id":5747799,"id":"Q5747799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$4C0A5593-307C-4DAE-B106-E70CBF1145EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"328caad0b77361ed511af273d18672e961160188","datavalue":{"value":{"entity-type":"item","numeric-id":2655329,"id":"Q2655329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$BCCD6234-6A1C-499C-B1E6-F47262A64C07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11afb07be1b91dc20a196bc7b66e67e767c9bb31","datavalue":{"value":{"entity-type":"item","numeric-id":4874803,"id":"Q4874803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$3B49DAE9-95BA-4E78-86C6-EBB1A4FFCEF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e72d94f5a6b3850e86694683d94b9b8cd6b5a064","datavalue":{"value":{"entity-type":"item","numeric-id":2102932,"id":"Q2102932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$3E4F4C32-A41D-47FA-BDF4-96AC1EF2A25A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"559ec538d1ea8832b77e20dc9482163269827794","datavalue":{"value":{"entity-type":"item","numeric-id":6185789,"id":"Q6185789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$C5666744-AA17-47E5-9695-B8485574936B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2946f9210b56cf40c78bc7c781e28832ee6caf5f","datavalue":{"value":{"entity-type":"item","numeric-id":5541301,"id":"Q5541301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$F69185E8-885B-4CBC-93B2-1FCA953F2CF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"150e899548b8d3876b4b8eae7b467fc6bc2b4b1f","datavalue":{"value":{"entity-type":"item","numeric-id":2907328,"id":"Q2907328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$9C93AF14-22C6-4689-A85D-E808FFCF1918","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$86A13A48-56F0-4C7A-BAD6-DA13C1E0B544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"207e2abc983e205cc995a82c818767ccfaf564f2","datavalue":{"value":{"entity-type":"item","numeric-id":2987064,"id":"Q2987064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$3CE6DA6E-30EB-4AD0-AC2A-7C12388DE0D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72f2cf240c4f45db6b6b4000cb1318c1ca70491a","datavalue":{"value":{"entity-type":"item","numeric-id":2096443,"id":"Q2096443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$16521C18-46FE-456B-86C7-9DBBB5E42A04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8549a72adcf761e26ac06f668c8502d7f581da97","datavalue":{"value":{"entity-type":"item","numeric-id":3678266,"id":"Q3678266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$3D6230F1-C2D4-4C8D-B5C8-68159C74EF64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0000b092379f98c95c3775e7aba07202a86433b","datavalue":{"value":{"entity-type":"item","numeric-id":5495937,"id":"Q5495937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$DB14F193-C8D5-4AE9-9054-90EE8373A8B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"448244272da4dbff5b7c78c2545c59c5b5af64d9","datavalue":{"value":{"entity-type":"item","numeric-id":3102745,"id":"Q3102745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$D51FB90B-E949-4621-A2DC-0CA4F810029B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4da3d0430975e1c2b8bdd5aed76ce16937caeaf","datavalue":{"value":{"entity-type":"item","numeric-id":6934148,"id":"Q6934148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$C71C8841-C17B-48EC-99ED-64100B997A0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6893591$BFE89A70-D716-4962-90D5-9E77C1F5BBB6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem proving as constraint solving for coherent logic with function symbols","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theorem_proving_as_constraint_solving_for_coherent_logic_with_function_symbols"}}}}}