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 erheblichen Anwendungswert in vielen Bereichen, darunter die Verifizierung und Synthese von Software- und Hardware-Systemen.