Formule propositionnelle

Résumé

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). Propositions 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 connec

Source officielle

https://fr.wikipedia.org/wiki/Formule_propositionnelle

À 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 (7)

Publications associées

Chargement

Personnes associées (2)

Personnes associées

Chargement

Unités associées (1)

Unités associées

Chargement

Concepts associés (23)

Concepts associés

Chargement

Cours associés (9)

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.

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuitscombinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de synthèse de systèmelogiques sont étudiées et appliquée

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics as diverse as mathematical reasoning, combinatorics, discrete structures & algorithmic thinking.

Afficher plus

Cours associés

Chargement

Séances de cours associées (24)

Séances de cours associées

Chargement

, ,

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem for two subtheories of Boolean algebra, giving a sound procedure for propositional logical equivalence that is incomplete in general but complete with respect to a subset of Boolean algebra axioms. We first show a new algorithm to produce a normal form for expressions in the theory of ortholattices (OL) in time O(n^2). We also consider an algorithm, recently presented but never evaluated in practice, producing a normal form for a slightly weaker theory, orthocomplemented bisemilattices (OCBSL), in time O(n log(n)^2). For both algorithms, we present an implementation and show efficiency in two domains. First, we evaluate the algorithms on large propositional expressions, specifically combinatorial circuits from a benchmark suite, as well as on large random formulas. Second, we implement and evaluate the algorithms in the Stainless verifier, a tool for verifying the correctness of Scala programs. We used these algorithms as a basis for a new formula simplifier, which is applied before valid verification conditions are saved into a persistent cache. The results show that normalization substantially increases cache hit ratio in large benchmarks.

2022

Chargement

On Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Robin Steiger, Philippe Paul Henri Suter

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier-free BAPA (QFBAPA). Deciding the satisfiability of QFBAPA formulas has been shown to be NP-complete using an eager reduction to quantifier-free Presburger arithmetic that exploits a sparse-solution property. In contrast to many other NP-complete problems (such as quantifier-free first-order logic or linear arithmetic), the applications of QFBAPA to a broader set of problems has so far been hindered by the lack of an efficient implementation that can be used alongside other efficient decision procedures. We overcome these limitations by extending the efficient SMT solver Z3 with the ability to reason about cardinality constraints. Our implementation uses the DPLL(T) mechanism of Z3 to reason about the top-level propositional structure of a QFBAPA formula, improving the efficiency compared to previous implementations. Moreover, we present a new algorithm for automated decomposition of QFBAPA formulas. Our algorithm alleviates the exponential explosion of considering all Venn regions, significantly improving the tractability of formulas with many set variables. Because it is implemented as a theory plugin, our implementation enables Z3 to prove formulas that use QFBAPA constructs alongside constructs from other theories that Z3 supports (e.g. linear arithmetic, uninterpreted function symbols, algebraic data types), as well as in formulas with quantifiers. We have applied our implementation to verification of functional programs; we show it can automatically prove formulas that no automated approach was reported to be able to prove before.

2010

Chargement

, ,

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier-free BAPA (QFBAPA). in contrast to many other NP-complete problems (such as quantifier-free first-order logic or linear arithmetic), the applications of QFBAPA to a broader set of problems has so far been hindered by the lack of an efficient implementation that can be used alongside other efficient decision procedures. We overcome these limitations by extending the efficient SMT solver Z3 with the ability to reason about cardinality (QFBAPA) constraints. Our implementation uses the DPLL(T) mechanism of Z3 to reason about the top-level propositional structure of a QFBAPA formula, improving the efficiency compared to previous implementations. Moreover, we present a new algorithm for automatically decomposing QFBAPA formulas. Our algorithm alleviates the exponential explosion of considering all Venn regions, significantly improving the tractability of formulas with many set variables. Because it is implemented as a theory plugin, our implementation enables Z3 to prove formulas that use QFBAPA constructs with constructs from other theories that Z3 supports, as well as with quantifiers. We have applied our implementation to the verification of functional programs; we show it can automatically prove formulas that no automated approach was reported to be able to prove before.

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Chargement