Formule logique

Résumé

En logique on dit d’une suite finie de lettres qu’elle est une formule, ou parfois formule bien formée, d'un langage logique donné lorsqu’elle peut être construite en appliquant une combinaison des règles de la grammaire formelle associée, on parle de la syntaxe du langage. Informellement les formules sont les assemblages de lettres auxquels il est possible de donner une signification en termes de valeur de vérité (Vrai, ou Faux). Les formules logiques sont l'équivalent des phrases du langage naturel. Les formules du langage sont interprétées, suivant la sémantique de la logique considérée, en leur attribuant une valeur de vérité. La syntaxe du calcul des prédicats nécessite d'introduire une autre notion, celle de terme, la syntaxe des termes du langage étant liée à une signature. Les termes sont eux interprétés par des objets (nombres, points, etc.). Il est possible d'assembler les formules pour construire des démonstrations, suivant des règles formelles associées à un système de dé

Source officielle

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

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

Publications associées

Chargement

Personnes associées

Chargement

Unités associées

Chargement

Concepts associés (37)

Concepts associés

Chargement

Cours associés (8)

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.

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.

This is an introductory course in the theory of statistics, inference, and machine learning, with an emphasis on theoretical understanding & practical exercises. The course will combine, and alternate, between mathematical theoretical foundations and practical computational aspects in python.

Afficher plus

Cours associés

Chargement

Séances de cours associées (19)

Séances de cours associées

Chargement

On Polynomial Algorithms for Normalizing Formulas

Mario Bucev, Simon Guilloud, Viktor Kuncak

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

The Impact of Voice Leading and Harmony on Musical Expectancy

Robert Lieck, Markus Franz Josef Neuwirth, Martin Alois Rohrmeier

In Western tonal music, voice leading (VL) and harmony are two central concepts influencing whether a musical sequence is perceived as well-formed. However, experimental studies have primarily focused on the effect of harmony on the cognitive processing of polyphonic music. The additional effect of VL remains unknown, despite music theory suggesting VL to be tightly connected to harmony. Therefore, the aim of this study was to investigate and compare the effects of both VL and harmony on listener expectations. Using a priming paradigm and a choice reaction time task, participants (N = 34) were asked to indicate whether the final chord in a sequence had a different timbre than the preceding ones (cover task), with the experimental conditions being good and poor VL or harmony, respectively. An analysis with generalised mixed effects models revealed a significant influence of both VL and harmony on reaction times (RTs). Moreover, pairwise comparison showed significantly faster RTs when VL was good as compared to both VL and harmony being poor, which was not the case when only harmony was good. This study thus provides evidence for the additional importance of VL for the processing of Western polyphonic music.

2020

Chargement

Due to their complexity, the syntax of modern modeling languages is preferably defined in two steps. The abstract syntax identifies all modeling concepts whereas the concrete syntax should clarify how these concepts are rendered by graphical and/or textual elements. While the abstract syntax is often defined in form of a metamodel, there does not exist such standard format yet for concrete syntax definitions. The diversity of definition formats-ranging from EBNF grammars to informal text-is becoming a major obstacle for advances in modeling language engineering, including the automatic generation of editors. In this paper, we propose a uniform format for concrete syntax definitions. Our approach captures both textual and graphical model representations and even allows to assign more than one rendering to the same modeling concept. Consequently, following our approach, a model can have multiple, fully equivalent representations, but-in order to avoid ambiguities when reading a model representation-two different models should always have distinguishable representations. We call a syntax definition correct, if all well-formed models are represented in a non-ambiguous way. As the main contribution of this paper, we present a rigorous analysis technique to check the correctness of concrete syntax definitions.

Springer-Verlag2008

Chargement