Logique modale

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 . 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 quil pleut ;
Il est démontré qu'''il pleut ;
Il est obligatoire quil pleuve. Il existe une variété 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.

Logique modale aléthique En logique modale aléthique (ou aristotélicienne, ou classique), on dégage essentiellement quatre modalités :

nécessaire (ce qui ne peut pas ne pas être vrai), noté

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (8)

Publications associées

Chargement

Personnes associées

Chargement

Unités associées

Chargement

Concepts associés (51)

Concepts associés

Chargement

Cours associés (1)

Cours associés

Chargement

Séances de cours associées (2)

Séances de cours associées

Chargement

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

Acoustic-Labial Speaker Verification

Dominique Genoud

This paper describes a multimodal approach for speaker verification. The system consists of two classifiers, one using visual features and the other using acoustic features. A lip tracker is used to extract visual information from the speaking face which provides shape and intensity features. We describe an approach for normalizing and mapping different modalities onto a common confidence interval. We also describe a novel method for integrating the scores of multiple classifiers. Verification experiments are reported for the individual modalities and for the combined classifier. The performance of the integrated system outperformed each sub-system and reduced the false acceptance rate of the acoustic sub-system from 2.3% to 0.5%.

1997

Chargement

Improving biometric verification with class-independent quality information

Andrzej Drygajlo, Krzysztof Kryszczuk

Existing approaches to biometric classification with quality measures make a clear distinction between the single-modality applications and the multi-modal scenarios. This study bridges this gap with Q-stack, a stacking-based classifier ensemble, which uses the class-independent signal quality measures and baseline classifier scores in order to improve the accuracy of uni- and multi-modal biometric classification. The seemingly counterintuitive notion of using class-independent quality information for improving class separation by considering quality measures as conditionally relevant classification features is explained. The authors present Q-stack as a generalised framework of classification with quality information, and argue that existing methods of classification with quality measures are its special cases. The authors further demonstrate the application of Q-stack on the task of biometric identity verification using face and fingerprint modalities, and show that the use of the proposed technique allows a systematic reduction of the error rates below those of the baseline classifiers, in scenarios involving single and multiple biometric modalities.

2009

Chargement

Complex-coupled photonic crystal THz lasers with independent loss and refractive index modulation

Jérôme Faist, Romuald Houdré, Hua Zhang

Compared to near infra-red photonic crystal (PhC) band-edge lasers, achieving vertical emission with quantum cascade (QC) material operating in the THz range needs dedicated engineering because the TM polarized emission of QCLs favors in-plane emitting schemes and the currently used double plasmon waveguide, prevents vertical light extraction. We present an approach with independent refractive index and extraction losses modulation. The extraction losses are obtained with small extracting holes located at appropriate positions. The modal operation of the PhC is shown to critically depend on the external losses introduced. Very high surface emission power for optimum loss extractor design is achieved. (C) 2011 Optical Society of America

2011

Chargement

Logique

La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règle

Calcul des propositions

Le calcul des propositions ou calcul propositionnel, (ou encore logique des propositions) fait partie de la logique mathématique. Il a pour objet l'étude des relations logiques entre « propositions

Calcul des prédicats

En logique mathématique, le calcul des prédicats du premier ordre, ou calcul des relations, logique quantificationnelle, ou tout simplement calcul des prédicats, est un système formel utilisé pour rai