{"entities":{"Q7361682":{"pageid":31520585,"ns":120,"title":"Item:Q7361682","lastrevid":105367190,"modified":"2026-10-07T13:36:45Z","type":"item","id":"Q7361682","labels":{"en":{"language":"en","value":"First-Order Logic According to Fitting"}},"descriptions":{"en":{"language":"en","value":"AFP entry FOL-Fitting"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"252d624b5a33c56ea69beb71752e96c4f5e58515","datavalue":{"value":"https://isa-afp.org/entries/FOL-Fitting.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361682$651B4895-547B-416B-A3C8-67EE4869C7AB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"69b526f8f9b460c8b0495ed0dc1b16b6f66ea15a","datavalue":{"value":{"time":"+2007-08-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361682$7EB30689-563B-4D2E-BDB9-10CC58B97E94","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"42cc17b6ebd1e6b2e2779d5c2e7eb07525a54975","datavalue":{"value":"Stefan Berghofer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361682$47171597-5A72-4C6B-A966-55AD5428AF81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"812c10ac7a5795cec4f806d989a562680fd7fa78","datavalue":{"value":"Asta Halkj\u00e6r From","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361682$EA100A00-9456-45D4-85A3-439AC1890D7C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d52cef67fff487cd3b152f83cceb5d981e87a17a","datavalue":{"value":{"text":"First-Order Logic According to Fitting","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361682$6673232B-4775-487B-8BDE-F461FB72DF4F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1c75d99c351435d04b8ee4afb737f56320cd885f","datavalue":{"value":"We present a formalization of parts of Melvin Fitting's book \"First-Order Logic and Automated Theorem Proving\". The formalization covers the syntax of first-order logic, its semantics, the model existence theorem, a natural deduction proof calculus together with a proof of correctness and completeness, as well as the L\u00f6wenheim-Skolem theorem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361682$0CA3137D-710E-465C-9B09-D27F2E25AF3E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ad2e3e71fd34316c4d5dca241131f17edc1acca","datavalue":{"value":{"entity-type":"item","numeric-id":4863622,"id":"Q4863622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361682$BA19BF15-EE57-4DF8-9AAB-23B337FC95C2","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":"Q7361682$350CC327-035F-4124-9CB5-FC9ABB6CEB19","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"04648103e40c59982614f3813f352c9cf3f67ce8","datavalue":{"value":{"entity-type":"item","numeric-id":7360808,"id":"Q7360808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361682$E07EDCAF-05F9-4C70-860F-9D43EC9D0290","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":"Q7361682$EE59F1E6-A23A-4C56-9C8E-C9ACBE162FA8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"First-Order Logic According to Fitting","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/First-Order_Logic_According_to_Fitting"}}}}}