Automatisches Theorembeweisen

Das Ziel des automatischen Beweisens ist es, Beweise in einer formellen Sprache automatisch zu generieren, wenn eine Vermutung (Zieltheorem) und eine Wissensbasis bekannter Fakten gegeben sind. Diese Technologie hat erhebliche Anwendungen in der Verifizierung und Synthese von Software- und Hardware-Systemen, unter anderem.