Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
En logique mathématique une proposition, ou formule propositionnelle, ou expression propositionnelle est une expression construite à partir de connecteurs et de variables propositionnelles. En logique propositionnelle classique, une formule propositionnelle, ou expression propositionnelle, est une formule bien formée qui possède une valeur de vérité. Si les valeurs de toutes les variables propositionnelles dans une formule propositionnelle sont données, une unique valeur de vérité peut être déterminée. Une formule propositionnelle est construite à partir de propositions simples, telles que « cinq est supérieur à trois », ou de variables propositionnelles telles que P et Q, en utilisant des connecteurs logiques tels que NON, ET, OU et IMPLIQUE ; par exemple : (P ET NON Q) IMPLIQUE (P OU Q). Dans le calcul des propositions, les propositions de base sont simples ou atomiques (on ne peut pas les décomposer). Les propositions atomiques sont liées par des connecteurs propositionnels, les plus courants sont «ET», «OU», «SI ... ALORS ...», «ni ... ni ...», « ... EST ÉQUIVALENT À ...» . En langue vernaculaire des mathématiciens, le point-virgule « ; » et le conjonctif « MAIS » sont considérés comme des expressions de « ET ». Une suite de propositions sont considérées comme liées par des conjonctions, et l'analyse formelle applique une « règle de parenthèses » récursive. Les propositions simples sont de nature déclarative, elles affirment quelque chose au sujet de l'état du monde, par exemple « Cette vache est bleue », « Il y a un coyote! », « ce triangle est isocèle », « 3 ≥ 5 ». Un système formel est un ensemble de symboles, appelés variables, un ensemble de symboles appelés connecteurs (*, +, ~ , &, V, =, ≡, ⋀, ¬) et un système de règles pour manipuler les symboles. Analyse : Dans le raisonnement déductif, les philosophes, rhéteurs et mathématiciens réduisent les arguments à des formules, puis les étudient pour vérifier leur exactitude.
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having po ...