Die computergestützte Mechanisierung unterschiedlicher Logikformalismen ist
Gegenstand einer Konferenz vom 1. bis 7. August 2015 am Fachbereich
Mathematik und Informatik der Freien Universität Berlin. Unter dem Titel
„Conference on Automated Deduction“ (CADE) befassen sich die Teilnehmer aus
dem In- und Ausland vornehmlich mit der Methode des Automatischen
Theorembeweisens. Dabei werden mathematische bzw. logische Beweise
vollautomatisch durch den Computer gefunden. Unter Beweis wird hier eine
präzise Argumentationskette verstanden, die ein Beweisziel (das Theorem)
aus Grundannahmen (den Axiomen) ableitet. Erörtert wird auch, wie die
automatische Deduktion beispielsweise in der Informatik und Mathematik
angewendet werden kann.