Logique modale

Certaines informations figurant dans cet article ou cette section devraient être mieux reliées aux sources mentionnées dans les sections « Bibliographie », « Sources » ou « Liens externes » (avril 2015).

Vous pouvez améliorer la vérifiabilité en associant ces informations à des références à l'aide d'appels de notes.

Cet article n’est pas rédigé dans un style encyclopédique (avril 2015).

Vous pouvez améliorer sa rédaction !

En logique mathématique, une logique modale est un type de logique formelle qui étend la logique propositionnelle, la logique du premier ordre ou la logique d'ordre supérieur avec des modalités. Une modalité spécifie des qualités du vrai^[pas clair]. Par exemple, une proposition comme « il pleut » peut être précédée d'une modalité :

• Il est nécessaire qu'il pleuve ;
• Demain, il pleut ;
• Christophe Colomb croit qu'il pleut ;
• Il est démontré qu'il pleut ;
• Il est obligatoire qu'il pleuve.

Il existe toutes sortes de logiques modales comme les logiques temporelles, la logique épistémique (logique de connaissance). En informatique, la logique modale est utilisée pour son expressivité et les aspects algorithmiques. Par exemple, la logique temporelle est utilisée pour spécifier des programmes puis les vérifier.