Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
L’objectif de cette thèse est de concevoir un calcul d’hypersequents appelé HMR pour la Logique Modale de Riesz, ou de manière équivalente, pour la théorie équationnelle des espaces de Riesz modaux. Elle s’inscrit dans une ligne de recherche visant à fournir un système de preuve structurelle pour des logiques probabilistes bien connues comme le µ–calcul probabiliste ou la logique probabiliste du temps arborescent (probabilistic Computational Tree Logic or pCTL). La logique modale de Riesz est une logique modale à valeurs réelles, c’est-à-dire une logique modale dont les termes sont interprétés comme des nombres réels au lieu de Booléens. Si elle est étendue avec des opérateurs de point fixes, la logique modale de Riesz est suffisamment expressive pour coder la plupart des logiques probabilistes habituelles comme la logique probabiliste du temps arborescent mentionnée ci-dessus. De plus, une axiomatisation équationnelle a été fournie pour la logique modale de Riesz : il existe un ensemble d’axiomes tels que deux termes de la logique modale de Riesz sont équivalents, c’est-à-dire qu’ils ont les mêmes interprétations dans tous les modèles, si et seulement s’ils peuvent être prouvés égaux en utilisant cet ensemble d’axiomes et les règles du raisonnement équationnel. Le but de fournir un calcul d’hypersequents pour la logique modale de Riesz est d’avoir un système de preuve ayant certaines propriétés intéressantes. La principale limite du raisonnement équationnel est que ses règles ne sont pas toutes analytiques : il peut être nécessaire de « deviner » des formules lors de la construction d’une dérivation, ce qui demande une certaine ingéniosité humaine. Par conséquent, nous voulons fournir un système de preuve à la fois correct et complet en ce qui concerne l’axiomatisation de la logique modale de Riesz, tout en n’ayant que des règles analytiques, ce qui rend le processus de construction des dérivations beaucoup plus simple. Pour ce faire, nous nous appuyons sur un autre calcul d’hypersequents existant introduit ...