Automated Theorem Prover

Abstract

Het doel is om een automatische stelling bewijzer te maken. Hierin kan men model van de wereld maken en daarop predikaatlogische formules testen op waarheid. Dit kunnen zelfgemaakte modellen zijn of meegeleverde standaard modellen. Bij het testen op waarheid wordt er door de tool een bedeling gegeven die de formule waar maakt als er vrije variabelen in de formule aanwezig zijn. Het doeleinde van de scriptie is om de tool te kunnen gebruiken in de cursus Inleiding Logica van de bachelor Kunstmatige Intelligentie.