{"entities":{"Q7361652":{"pageid":31520495,"ns":120,"title":"Item:Q7361652","lastrevid":105366914,"modified":"2026-10-07T13:36:43Z","type":"item","id":"Q7361652","labels":{"en":{"language":"en","value":"Propositional Proof Systems"}},"descriptions":{"en":{"language":"en","value":"AFP entry Propositional_Proof_Systems"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"19aec7ed33a3570ef2a91d9c21cd32e91c458b09","datavalue":{"value":"https://isa-afp.org/entries/Propositional_Proof_Systems.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361652$5D960E7A-154A-403A-AF40-A547C149B199","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2f889432403f3e87ba72d1eb34a5f814171f1311","datavalue":{"value":{"time":"+2017-06-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361652$6CBC6DE4-4813-4A05-ACC4-CCE058E5F1C6","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"045dde749400578820aeaa85be8498af97b18250","datavalue":{"value":"Julius Michaelis","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361652$B8AF873C-AED4-4FA6-B8FD-A712B852BEEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361652$FD444D5D-8409-4B32-8E01-92E0C02A4E1D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6e531ba81454696d56091791f93f6a22aac6c2c4","datavalue":{"value":{"text":"Propositional Proof Systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361652$C2746B40-0247-40C9-AD78-F3DBF36F230C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fff6e46ddde969885c821ad80b14a4b94c7c9424","datavalue":{"value":"We formalize a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) and prove the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361652$F81DF2DA-3A3D-44A3-8E75-04A00CE17CE0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8971435217b64c50e375aec68a6c58475d8d0dd9","datavalue":{"value":{"entity-type":"item","numeric-id":3249759,"id":"Q3249759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$2BA7EA40-5DD2-44B8-8137-E7AB714642B5","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":"Q7361652$6DE2C3D9-0924-48FF-A17A-EAF52F032CAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$11EB1DD6-D678-4EA2-A6B0-8E7F50080C72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$15474979-68C8-4F88-AE4C-EFA88D786AAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12143b60940a94520e674629cc78749e74e38ed6","datavalue":{"value":{"entity-type":"item","numeric-id":1437031,"id":"Q1437031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$768BFD69-32FC-4770-AC05-B23F2ABE20DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"672be30d9c0fd1bb08a1fc6131d1506ec245277a","datavalue":{"value":{"entity-type":"item","numeric-id":4830107,"id":"Q4830107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$8B1807E1-1995-4549-95CB-5F2D24F70675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8bc1b66416e18542f53f888ff4b3cb8b2c1c8a8c","datavalue":{"value":{"entity-type":"item","numeric-id":5764366,"id":"Q5764366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$3A97ECD7-2F5F-45AA-B4DA-0A2443B9C0F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17712a187dc84422a99627a8301b6f187b072f31","datavalue":{"value":{"entity-type":"item","numeric-id":3777983,"id":"Q3777983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$95024405-50A9-456C-B64A-E42A53B2C266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"033624a7007e7f19014ffd926803b277854e28c1","datavalue":{"value":{"entity-type":"item","numeric-id":5729293,"id":"Q5729293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$6C84E32D-83F3-4C65-A69D-1D036EFCF2B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$8B660558-1361-4850-B8B0-D64FD730128A","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$964F10F2-131C-478D-88A6-768B096F3CDF","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"0010e22d998484f218097f7f79d7fc22bc7427c6","datavalue":{"value":{"entity-type":"item","numeric-id":7360817,"id":"Q7360817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$16BC7DCB-33D1-4E95-923F-B1D46899DE9F","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361652$2C727323-F422-4063-997A-0750C9984ECE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Propositional Proof Systems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Propositional_Proof_Systems"}}}}}