**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.

Concept# Atomic formula

Summary

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.

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (25)

Related people (3)

Related concepts (16)

Related courses (4)

Related units (1)

Related lectures (32)

Quantifier (logic)

In logic, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula. For instance, the universal quantifier in the first order formula expresses that everything in the domain satisfies the property denoted by . On the other hand, the existential quantifier in the formula expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widest scope is called a quantified formula.

Term (logic)

In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact. A first-order term is recursively constructed from constant symbols, variables and function symbols. An expression formed by applying a predicate symbol to an appropriate number of terms is called an atomic formula, which evaluates to true or false in bivalent logics, given an interpretation.

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.

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

Introduction to Quantifier Elimination for Presburger Arithmetic

Introduces formal verification methodology and Presburger arithmetic for program verification and automated reasoning.

Propositional Logic: Equivalence and Normal Forms

Covers propositional logic, equivalence proofs, and normal forms using truth tables.

Propositional Logic: Equivalence and Normal Forms

Covers propositional logic, logical equivalence, tautology, contradiction, and normal forms.

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 ...

2024Viktor Kuncak, Simon Guilloud, Mario Bucev

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 ...

2022The intermetallic compound PdGa has recently attracted considerable interest for combining high catalytic activity with high reaction selectivity in symmetric heterogeneous catalysis, in particular semi-hydrogenation of acetylene and methanol steam reformi ...