{"entities":{"Q7361657":{"pageid":31520510,"ns":120,"title":"Item:Q7361657","lastrevid":105366953,"modified":"2026-10-07T13:36:43Z","type":"item","id":"Q7361657","labels":{"en":{"language":"en","value":"A Sequent Calculus for First-Order Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry FOL_Seq_Calc1"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"78215760d258ddfb0287073faa67cbe22330d82a","datavalue":{"value":"https://isa-afp.org/entries/FOL_Seq_Calc1.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361657$C947FA42-C9D2-400F-888A-0EB1D024C5C6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ffdc9ffce048cac45801362823035df6483c760","datavalue":{"value":{"time":"+2019-07-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361657$9B37C21C-787A-4B44-8D5B-44F17209AC75","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"812c10ac7a5795cec4f806d989a562680fd7fa78","datavalue":{"value":"Asta Halkj\u00e6r From","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361657$56E7CA42-10D0-4554-B1C5-F31644F31652","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"db387998486ce4a251c290a1ea4b72600edbf89e","datavalue":{"value":"Alexander Birch Jensen","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361657$FF571223-915F-4973-A679-ABBB06A7A123","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f19e42813e41b1b694ee6662dce0e445e8e41f4b","datavalue":{"value":"Anders Schlichtkrull","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361657$800AEC19-5185-4D60-ABC7-2376A0220622","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"fad673ab88e4c617ff7ef906721c9d50cfb4df35","datavalue":{"value":"J\u00f8rgen Villadsen","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361657$2A985AF5-DAFE-4E5A-BA33-1CFF4F1654E0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"eca4c1cc1369d5a51de1d8545f4c4d579c535afd","datavalue":{"value":{"text":"A Sequent Calculus for First-Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361657$9A85D6E8-E3A9-41B2-A453-F48AE93EC176","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1ab2ce4c9b143caacf1729a1908be156eb730dfa","datavalue":{"value":"This work formalizes soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a complete semantic tableau calculus, the proof of which is based on the First-Order Logic According to Fitting theory. The calculi and proof techniques are taken from Ben-Ari's Mathematical Logic for Computer Science. Papers: ceur-ws.org/Vol-3002/paper7.pdf and doi.org/10.1093/logcom/exad013 .","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361657$FDFDA798-8A03-4761-90BF-278F9D3661AB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"95f5e5a42b14858827b86e355a072cbbd1bdb099","datavalue":{"value":{"entity-type":"item","numeric-id":2894076,"id":"Q2894076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361657$E21CBE88-E448-4548-B445-FA3D2847307C","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":"Q7361657$172C7FF0-F0B3-4BE6-836F-3C9D34983B26","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"5b23589eced77217122b2d223cf1e7808fbf0972","datavalue":{"value":{"entity-type":"item","numeric-id":7361682,"id":"Q7361682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361657$A82E9AFF-83D2-4F38-B1D6-EEB696E66E85","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":"Q7361657$61A8AA9D-ACB3-4609-BC5C-06A41C0DEFDE","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":"Q7361657$520EF8CB-80BC-4307-94F6-A2129C1FD025","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Sequent Calculus for First-Order Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Sequent_Calculus_for_First-Order_Logic"}}}}}