In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic. Compound formulas are formed by combining the atomic formulas using the logical connectives. The precise form of atomic formulas depends on the logic under consideration; for propositional logic, for example, a propositional variable is often more briefly referred to as an "atomic formula", but, more precisely, a propositional variable is not an atomic formula but a formal expression that denotes an atomic formula. For predicate logic, the atoms are predicate symbols together with their arguments, each argument being a term. In model theory, atomic formulas are merely strings of symbols with a given signature, which may or may not be satisfiable with respect to a given model. The well-formed terms and propositions of ordinary first-order logic have the following syntax: Terms: that is, a term is recursively defined to be a constant c (a named object from the domain of discourse), or a variable x (ranging over the objects in the domain of discourse), or an n-ary function f whose arguments are terms tk. Functions map tuples of objects to objects. Propositions: that is, a proposition is recursively defined to be an n-ary predicate P whose arguments are terms tk, or an expression composed of logical connectives (and, or) and quantifiers (for-all, there-exists) used with other propositions. An atomic formula or atom is simply a predicate applied to a tuple of terms; that is, an atomic formula is a formula of the form P (t1 ,..., tn) for P a predicate, and the tn terms. All other well-formed formulae are obtained by composing atoms with logical connectives and quantifiers. For example, the formula ∀x. P (x) ∧ ∃y. Q (y, f (x)) ∨ ∃z. R (z) contains the atoms As there are no quantifiers appearing in an atomic formula, all occurrences of variable symbols in an atomic formula are free.

À 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.
Cours associés (4)
CS-101: Advanced information, computation, communication I
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 a
CS-550: Formal verification
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 u
MATH-664: Malliavin calculus and normal approximations
This course will provide a basic knowledge of the stochastic calculus of variations with respect to the Brownian motion. A variety of applications will be presented including the regularity of probabi
Afficher plus
Publications associées (25)

From trees to barcodes and back again II: Combinatorial and probabilistic aspects of a topological inverse problem

Kathryn Hess Bellwald, Lida Kanari, Adélie Eliane Garin

In this paper we consider two aspects of the inverse problem of how to construct merge trees realizing a given barcode. Much of our investigation exploits a recently discovered connection between the symmetric group and barcodes in general position, based ...
2024
Afficher plus
Unités associées (1)
Concepts associés (16)
Quantification (logique)
vignette|Symboles mathématiques des deux quantificateurs logiques les plus courants.|236px En mathématiques, les expressions « pour tout » (ou « quel que soit ») et « il existe », utilisées pour formuler des propositions mathématiques dans le calcul des prédicats, sont appelées des quantifications. Les symboles qui les représentent en langage formel sont appelés des quantificateurs (ou autrefois des quanteurs). La quantification universelle (« pour tout ... » ou « quel que soit ... ») se dénote par le symbole ∀ (un A à l'envers).
Terme (logique)
Un terme est une expression de base du calcul des prédicats, de l'algèbre, notamment de l'algèbre universelle, et du calcul formel, des systèmes de réécriture et de l'unification. C'est l'objet produit par une analyse syntaxique. Sa principale caractéristique est d'être homogène (il n'y a que des opérations de base et pas d'opérations logiques) et de décrire l'agencement des opérations de base. Un terme est parfois appelé une formule du premier ordre.
Ground expression
In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables. In first-order logic with identity with constant symbols and , the sentence is a ground formula. A ground expression is a ground term or ground formula. Consider the following expressions in first order logic over a signature containing the constant symbols and for the numbers 0 and 1, respectively, a unary function symbol for the successor function and a binary function symbol for addition.
Afficher plus

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.