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

By Gian Luca Pozzato,
Università degli Studi di Torino
April 2003


In this work we provide labelled sequent calculi for some standard conditional logics. Conditional logics extend classical logic by means of a conditional operator ⇒. They have a long history and recently they have found applications in several areas of knowledge representation and artificial intelligence.

In this work, we introduce labelled sequent calculi for the conditional logic CK as well as for its standard extensions CK+ID, CK+MP and CK+MP+ID. We also exploit the calculi in order to describe a decision procedure for CK in polynomial space.

An implementation in Prolog and Java of the sequent calculi is also provided.