Sammanfattning Jag presenterar en formalisering i Isabelle/HOL av upplösningskalkylen för första ordningens logik med formella soliditets- och fullständighetsbevis. För att bevisa kalkylljudet använder jag substitutionslemma, och för att bevisa det fullständigt använder jag Herbrands tolkningar och semantiska träd. Korrespondensen mellan otillfredsställande uppsättningar av klausuler och ändliga semantiska träd formaliseras i Herbrands sats. Jag diskuterar de svårigheter som jag hade med att formalisera bevisen på den lyftande lemma som finns i litteraturen, och jag formaliserar ett korrekt bevis. Det fullständiga beviset är genom induktion på storleken på ett ändligt semantiskt träd. I hela papperet betonar jag detaljer som ofta slätas över i pappersprov. Jag ger en grundlig översikt över formaliseringar av första ordningens logik som finns i litteraturen. Formaliseringen av upplösningen är en del av IsaFoL-projektet, som är ett försök att formalisera logiken i Isabelle/HOL.
Berghofers arbete utvidgades nyligen av Schlichtkrull REF för att bevisa att första ordningens resolution var fullständig.
Formalization of the Resolution Calculus for First-Order Logic
{'venue': 'Journal of Automated Reasoning', 'journal': 'Journal of Automated Reasoning', 'mag_field_of_study': ['Mathematics', 'Computer Science']}