Lab for Automated Reasoning and Analysis LARA

More on Interpretations. Herbrand Theorem

In this continuation of lecture09, we discuss the foundations behind automated theorem provers for first-order logic. We describe a procedure that, given enough time, will prove any valid formula of first-order logic.

More on Interpretations

Decision Problem for Validity in First-Order Logic

 
sav08/lecture10.txt · Last modified: 2008/03/20 19:07 by vkuncak
 
© EPFL 2018 - Legal notice