Deduzione automatica per logiche condizionali:
analisi e sviluppo di un theorem prover