Maksimović, Petar
[Author]
;
Nice
[Contributor];
Univerzitet u Novom Sadu
[Contributor];
Liquori, Luigi
[Contributor];
Ghilezan, Silvia
[Contributor]
Développement et vérification des logiques probabilistes et des cadres logiques ; Development and verification of probability logics and logical frameworks
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Développement et vérification des logiques probabilistes et des cadres logiques ; Development and verification of probability logics and logical frameworks
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
On présente une Logique Probabiliste avec des opérateurs Conditionnels - LPCP, sa syntaxe, sémantique, axiomatisation correcte et fortement complète, comprenant une règle de déduction infinitaire. On prouve que LPCP est décidable, et on l'étend pour qu’il puisse représenter l'évidence, en créant ainsi la première axiomatisation propositionnelle du raisonnement basé sur l'évidence. On codifie les Logiques Probabilistes LPP1Q et LPPQ2 dans l'Assistant de Preuve Coq, et on vérifie formellement leurs propriétés principales: correction, complétude fort et non-compacité. Les deux logiques étendent la Logique Classique avec des opérateurs de probabilité, et présentent une règle de déduction infinitaire. LPPQ1 permet des itérations des opérateurs de probabilité, lorsque LPPQ2 ne le permet pas. On a formellement justifié l'utilisation des solveurs SAT probabilistes pour vérifier les questions liées à la cohérence. On présente LFP, un Cadre Logique avec Prédicats Externes, en introduisant un mécanisme pour bloquer et débloquer types et termes dans LF, en permettant l'utilisation d’oracles externes. On démontre que LFP satisfait tous les principales propriétés et on développe un cadre canonique correspondant, qui permet de prouver l’adéquation. On fournit diverses encodages - le λ-calcul non-typé avec la stratégie de réduction CBV, Programmation-par-Contrats, un langage impératif avec la Logique de Hoare, des Logiques Modales et la Logique Linéaire Non-Commutative, en montrant que en LFP on peut codifier aisément des side-conditions dans l'application des règles de typage et atteindre une séparation entre vérification et computation, en obtenant des preuves plus claires et lisibles. ; We introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary inference rule. We prove the obtained formalism decidable, and extend it so as to represent evidence, making it the first propositional axiomatisation of reasoning about ...