Eine Formel, die keine logischen Junktoren (wie ∧, ∨, →, ¬) und keine Quantoren enthält; in der Prädikatenlogik ist eine atomare Formel (Atom) typischerweise ein Prädikatsymbol angewandt auf ein Tupel von Termen (einschließlich Gleichheitsatomen) und dient als unteilbares Bauelement komplexer Formeln.

Prinzip

Atomare Formeln repräsentieren elementare Aussagen über Terme; komplexe Sätze werden durch Kombination von Atomen mit logischen Junktoren und Quantoren gebildet, und viele Beweissysteme reduzieren das Schließen auf Manipulationen von Atomen (z. B. arbeitet die Resolution auf Klauseln, die aus Atomen und deren Negationen bestehen).

Demonstration

In der Prädikatenlogik sind Ausdrücke wie P(a,b) oder x = y (nach Instanziierung der Variablen) atomare Formeln; im Gegensatz dazu ist P(a) ∧ Q(a) nicht atomar, weil hier zwei Atome mit einem Junktor verbunden werden.

Fehlanwendung

Eine zusammengesetzte Formel wie R(x) ∨ S(y) oder ein quantifizierter Ausdruck ∀x P(x) als atomar zu behandeln in Algorithmen, die Atome erwarten, führt zu Fehlern (z. B. wenn ground atoms erwartet werden).

Konsequenz

Atome liefern die Basiselemente für syntaktische Normalformen (Konjunktive/Disjunktive Normalform, Klauseln) und für automatisiertes Schließen: Identifikation und Manipulation von Atomen sind wesentlich für Unifikation, Resolution, Modellkonstruktion und Tableau-Methoden.

Umkehrung

Eine molekulare Formel ist die Umkehrung: jede Formel, die durch Anwendung von Junktoren oder Quantoren auf Atome gebildet wird, deren Bedeutung von der Komposition abhängt und die sich nicht auf eine einzelne Prädikatsanwendung reduziert.

Abgrenzung

In der Aussagenlogik sind atomare Formeln propositionale Variablen; in der Prädikatenlogik umfassen Atome Prädikatanwendungen und Gleichheit; einige erweiterte Logiken führen eingebaute Junktoren oder höherstufige Atome ein, was den Begriff des Atomaren verändert.

Semantische Spannung

Spannung besteht zwischen »atomare Formel« und »atomarer Satz« (erstere kann freie Variablen enthalten, letztere ist geschlossen) sowie zwischen Ground-Atoms (keine Variablen) für Model-Checking und allgemeinen Atomen in Beweiskalkülen.

Synthese

Eine atomare Formel ist die irreduzible Aussage einer logischen Sprache: ein Prädikat (oder Gleichheit) angewendet auf Terme, die Grundlage, aus der komplexe Formeln, Normalformen und automatisierte Schließverfahren aufgebaut werden.