What is semantics in propositional logic

Next: Predicate Logic Up: Logic Previous: Propositional Logic Syntax

Propositional Logic Semantics

Definition 1.8: semantics of propositional logic

The elements of the set {0,1} are called truth values. An assignment or interpretation is a function

. One expands to a function as follows:

1. For every atomic formula is .

Definition 1.9: inferability

Be S. a signature, A. a formula set and F. a formula, so and . Out A. follows F., short if for all interpretations or assignments applies: if , then .
Calculus

A calculus is a collection of purely `` mechanically '' applicable syntactic transformation rules.

The concept of derivability is in the foreground here. The deducibility is based on the syntax, the inference refers to the semantics of propositional logic. One formula F. is from a set of formulas A. derivable, if one F. out A. as well as certain logical axioms by means of a rule of inference, the so-called modus ponens.

Definition 1.10: Logical axioms

Be S. a signature and .

is called the set of logical axioms for the signature S..

Definition 1.11: derivability

Be S. a signature, and . F. is off A. derivable, short if there is a consequence in gives with the following properties:
1. For all i = 1, ... n applies: or there is j < i and k < i With .
2. Such a consequence is called a derivative of F. out A..

How does a derivative of F. out A. conditions?
• A sequence of derivations that has already been generated can be based on a logical axiom and a formula A. extend.
• If there is a formula in a derivation sequence that has already been created G and a formula before, so may the sequence around the formula H be extended. This type of lengthening is called modus ponens.
With the concept of deducibility one has fully grasped the content of the concept of inferability:

Theorem 1.2: correctness

Be S. a signature, . Then the following applies: If , then .

Theorem 1.3: Completeness

Be S. a signature, . Then the following applies: If , then .
resolution

The resolution is an easy one to apply syntactic Transformation rule. In one step, a third formula is generated from two formulas, provided they meet the requirements for the application of the resolution rule, which can then be used as an input in further resolution steps.

Definition 1.12: Resolution

Be and R. Clauses. Then is called R. Resolvent of and if it's a literal L. gives with and and R has the form:

Here is defined as

This fact can be shown in the following diagram:

...

Theorem 1.4: Resolution lemma

Let F be a formula in CNF, represented as a set of clauses. Furthermore, let R be a resolvent of two clauses and in F. Then F and equivalent to.

Definition 1.13: Resolvent

Be F. a set of clauses. Then Res(F.) defined as

Also put:

and finally be

Theorem 1.5: Resolution theorem of propositional logic

A set of clauses Fis unsatisfiable if and only if

Definition 1.14: consistency

Be S. a signature and . A. is called consistent if there is no formula gives with and .

Definition 1.15: completeness

Be S. a signature and . A. means complete, if for each applies: or .

Definition 1.16: model

An interpretationis called a model of A., if , i.e. any formula applies under the assignment or interpretation . One also writes: is a model of A..

If for a formula , so one writes: i.e.is not a model forG.

Definition 1.17: Minimal model

An interpretationis called a minimal model of A., if a model of A. is and there is no interpretation there that is also a model of A. is and . You write for the minimal model .

Theorem 1.6: Model Lemma

Let S be a signature. Then the following applies: For every consistent set of formulas A there is a model of A.

Definition 1.18: satisfiability

One formula F. means satisfiable, if F. owns at least one model, otherwise it is called F. unattainable.

A lot of formulas A. is called satisfiable if there is an occupancy there that for each formula in A. is a model.

Definition 1.19: tautology

One formula F. is called valid (or tautology) if each is to F. suitable occupancy a model for F. is.

Notation: if F. is a tautology and if F. is not a tautology.

Next: Predicate Logic Up: Logic Previous: Propositional Logic Syntax
Uschi Robers6.2.1998