Automatisches Beweisen

In diesem Zweig der künstlichen Intelligenz wurden in erster Linie Methoden entwickelt, um die bereits erwähnte kombinatorische Explosion möglichst gering zu halten. Methoden mit Hilfe derer man nach mechanischen, also programmierbaren Verfahren logisch korrektes Schließen nachvollziehen kann, wurden bereits vor der Entwicklung der ersten elektronischen Rechenmaschine von Mathematikern wie Hilbert, Gentzen, Skolem und anderen entwickelt.^3.3 Diese Verfahren stellten sich jedoch für den praktischen Gebrauch in Computerprogrammen als zu wenig effizient, das heißt, zu zeitraubend heraus. Als eine der bekanntesten Entwicklungen auf dem Gebiet des automatischen Beweisens ist das Resolutionsverfahren von Robinson Robinson[Rob65] zu nennen. Dies ist ein Beweisverfahren mit nur einer einzigen Ableitungsregel oder besser einem einzigen Ableitungsregelschema. Allerdings handelt es sich dabei weniger um eine Nachbildung des menschlichen logischen Schließens, als um eine speziell für Maschinen entwickelte Methode.