Logic¶

Basics¶

Logics are the basics of deductive databases
How to generate knowledge?
1. Axioms: Start with knowledge which is considered true
2. Inference: Derive new knowledge
Types of inference:
- Inductive Inference:
  - Draw conclusions from multiple observations
  - e.g., natural science
- Deductive Inference:
  - Axioms are given
  - Generate conclusions (theorems) from true facts (axioms) using rules
  - Focus of this lecture

History¶

Sophism
- 5th century BC
- Sophists were like teachers
- Teach rhetoric for money
  - Try to convince people using fallacious reasoning
  - Use ambiguities of languge
Aristotle
- 330 BC
- First appearance of formal logics
- Goal:
  - Derive new knowledge from old knowledge
  - Formal and safe inference
- Logic as tool for valid philosophical arguments
- Discovered Sophists’ tricks
  - Fallacy of Equivocation
    - Feather is light. Light can not be dark. A feather can not be dark.
  - Fallacy of Composition
    - Each individual vote is rational. Therefore, combining multiple votes is rational.
  - Fallacy of Accident
    - Cutting people with knives is a crime. Surgeons cut people with knives. Surgeons are criminals.
  - Fallacy of Begging the Question

Other Logics¶

Propositional Logic¶

Often referred as zero-order logic
Components:
- Atomic statement: Statement that can not be further divided (true of false)
- Connectives: AND, OR, IMPLICATION (truth function)
Bivalent logic
- Only true and false
- Counterpart of multi-valued logics (e.g., Fuzzy logic)
400 BC: Aristotle
- Wrote the book Metaphysics
- Base of propositional logic
- A statement AND its contradiction can not be true at the same time.
- A statement OR its contradiction has to be true.
- Invented the technique of indirect proofs
1847: George Boole
- First sound and complete formalization for truth values with algebraic calculus
- Invented Boolean Algebra
- Graphic representation by Venn diagrams
1879: Gottlob Frege
- Formalized first calculus with implications
1910: Bertrand Russel
- Refine Frege’s calculus
Problems:
- Does not investigate the statements themselves
  - e.g., for with variables does the statement hold
  - Bad for deductive databases
- No quantifiers/predicates

Term Logic¶

Introduced by Aristotle
Purpose: Allow deductive inference

Constructs¶

Term:
- Word represents something
- Has no truth value
- Just objects (e.g., man, blue)
Proposition:
- Combination of two terms
- Truth value: Either true or false
- Have Quantity:
  - Universal (all)
  - Existential/Particular (some)
- Have Quality:
  - Affirmative (e.g., is)
  - Negative (e.g., is not)
- Combinations:
  - Universal affirmative (UA): \( \forall \)
  - Existential affirmative (PA): \( \exists \)
  - Universal negative (UN): \( \neg\forall \)
  - Existential negative (PN): \( \neg \exists \)
Syllogism:
- Inference where a proposition (conclusion) follows two other propositions (premise)
- \( \text{Minor premise} \land \text{Major premise} \Rightarrow \text{Conclusion} \)
- Components:
  - Minor premise: Contains a minor term and and middle term
    - Minor term: Subject
    - Middle term: Predicate
  - Major premise: Contains the middle term and the major term
    - Middle term: Subject
    - Major term: Predicate
  - Conclusion: Contains the minor term as subject and the major term as predicate
- Important: The middle term must appear as predicate and as subject

Inference¶

Example (UA-UA-UA):
- Minor premise: All Greeks (subject) are men (predicate).
- Major premise: All men (subject) are mortal (predicate).
- Conclusion: All Greeks are mortal.
Results in 24 valid types of syllogisms
- Based on allowed conversations
- UA-UA-UA
- UN-UA-UN
- PN-UA-PN
- etc.
Square of opposition:
- Allow for logical conversions
- UA is contradiction of PN
- PA is contradiction of UN
Problem: No singulars in statements possible
- All terms are universally quantifed
- e.g., Every Socrates is a philosopher (Socrates is only a person)

Port-Royal-Logic¶

Arnauld/Nicole, 1662
Idea: Introduce singulars as universal
e.g., All Socrates are men.
Looks awkward/weird

Criticism¶

4th century BC: Eubulides of Miletus
- e.g., A grain of sand is no heap. Adding a single grain does not make a heap. => There is no heap of sand.
- Problem:
  - Natural language is not formal (not Aristotle’s fault)
  - Term Logic uses unary predicates
1879: Gottlob Frege
- Responsible for the downfall of Term Logic
- Recognized the need for quantifiable variables and predicates
- Distinction between object and concept
  - Morning Star is Venus
  - Venus is a planet
  - Subject/object are not reversible => Different is
- Results in predicate logic

Logicism¶

Based on Frege, 1879
Task:
- Axiomatize the new system of logic
- View mathematics as an extension of logic
- Build a mathematical logic for set theory
Foundation of analytic philosophy
- Analyse philosophical propositions
- Two trends: Neo-Positivism, Ideal language analysis
1901: Russel’s paradox:
- Frege’s logic still contained contradictions
- Imagine a barber shaving all people iff they do not shave themselves. Does the barber shave himself?
- Russel constructs a set containing the sets which are not member of themselves
Modern logical calculus:
- Book Principia Mathematica (by Russel and Whitehead)
- Use axiomatic set theory
- Idea: Find a complete and consistent set of axioms to derive every true theorem of the system
- Results in the Hilbert Program:
  - David Hilbert axiomatized all mathematics
Incompleteness theorem:
- Destruction by Kurt Gödel, 1931
- Complete axiomatization of all mathematics is not possible
- Incompleteness theorems
  1. If an axiomatic system is consistent, it can not be complete.
  2. The consistency of axioms can not be proved in the axiomatic system itself.
- But:
  - Gödel’s completeness theorem: Completeness of first-order logics

First-Order Logic¶

Basics¶

Central idea:
- Formally deduce from a set of facts
  - Which statements are true and which are false
  - Works due to the completeness theorem of FOL
- Introduces the concept of predicates
- Predicate: Property (group entities into types, e.g., man/student/strawberry)
- Fine-grained quantification: Existential + Universal
Formalization:
- Language:
  - Syntax
  - How to valid sentences look like?
- Interpretation:
  - Semantics
  - When is a statement true/false?
- System:
  - Mechanism called Deduction
  - What statements can be deduced from a given set?

Syntax¶

FOL syntax mimics natural language
Important: Syntax has no meaning (without interpretation)
Concepts:
- Formula (statement; basic building block)
- Predicate (express sth. about a term)
- Term (represent objects/concepts)
  - Constant
  - Variable (assign a value)
  - Function (apply on term)
Statement:
- Contains a predicate (something is said about entity, e.g., 3 is even)
- Can be concatenated to a new statement using special connectives, e.g., AND
- Has truth value
Quantification:
- Variables can be quantified
- Universal quantification:
  - Predicate must be valid for all valid substitutions of the variable
- Particular quantification:
  - Predicate must be valid for at least one valid substitution of the variable
Language
- Formal construction mechanism for statements

Signature¶

First-order logic language is quadruple (signature)
\( \mathcal{L}=(\Gamma, \Omega, \Pi, X) \)
\( \Gamma \):
- Non-empty finite set of constant symbols
- e.g., a, b, Hector, 3, Frog
- Constants may represent singular entities (but not types/collections)
\( \Omega \):
- Set of functions
- \( \Omega = \bigcup_{n\in\mathbb{N}} \Omega_n \)
\( \Pi \):
- Set of predicates
- \( \Pi = \bigcup_{n\in\mathbb{N}} \Pi_n \)
- \( \Pi_n \): Set of n-ary predicates
- e.g., \( P, Q, R \)
- Define sets of elements (constants evaluating predicates to true form a group)
- Evaluate to either true or false
- Substitution:
  - e.g., \( P(x|_{x=Hector}) \)
\( X \):
- Finite set of variables
- e.g., \( x,y,z \)
- Variables may only be substituted by constant values
- Higher-order logic: May substitute with predicates (increases complexity)
\( \mathcal{L} \):
- Signature of the language
- Signature is application-dependent
- The Universal signature is commonly used
  - Contains all predicates and functions of all aritys

Term¶

Constant:
- Represents objects or concepts
Variable:
- Assign a value (objects/concept)
- Gain expressiveness using variables
Function:
- Can be applied on terms
- e.g., 3+5 = +(3,5)
Term:
- Yet un-interpreted expression
- Built from constants, variables and functions
Have no truth value, e.g., 2+6
Definition \( T_\mathcal{L} \):
- Constant symbols from \( \Gamma \) are terms
- Variables from \( X \) are terms
- Functions \( f(t_1,\ldots,t_n) \) are terms iff \( f\in\Omega_n \) and \( t_1,\ldots,t_n \) are terms
Ground term:
- Term without any variables

../_images/02-term.png

Formula¶

Formulae are the basic building block (a statement)
- Inserting terms into predicates are atomic formula
- e.g., even(2+6)
- Yet un-interpreted statement
Classification of formulae:
- Atomic
- Open/Closed
- Rectified
- Grounded
Set of atomic formulas or Atom:
- \( A_\mathcal{L}=\{P(t_1,\ldots,t_n)\mid P\in\Pi_n, t_1,\ldots,t_n\in T_\mathcal{L}\} \)
- State simple facts, defined by predicates
Grounded formula:
- Formula without any variables
Recursive definition:
- Atomic formula is a formula
- If \( W \) is formula, \( \neg W \) is a formula
- If \( W_1 \) and \( W_2 \) are formulas, the following are formulas:
  - \( W_1 \land W_2 \)
  - \( W_1 \lor W_2 \)
  - \( W_1\Rightarrow W_2 \)
  - \( W_1\iff W_2 \)
- If \( x \) is variable and \( W \) is formula, \( \forall x(W) \) and \( \exists x(W) \) are formulas

../_images/02-formula.png

Connectives¶

Apply on formulae (i.e., connect or modify)
Have certain hierarchy (to avoid parenthesis):
1. Quantifiers (\( \forall, \exists \))
2. NOT (\( \neg \))
3. AND (\( \land \))
4. OR (\( \lor \))
5. Implication and Equivalence (\( \Rightarrow, \iff \))

Variable Bindings¶

Formula \( W \) has three sets of variables
- Free variables \( free(W) \)
- Bound variables \( bound(W) \)
- All variables \( vars(W)=free(W)\cup bound(W) \)
Recursive definition:
- Formula \( W \) is atomic:
  - \( free(W)=vars(W) \)
  - \( bound(W)=\emptyset \)
- Negation \( \neg W \):
  - Negation has no effect
  - \( free(\neg W)=free(W) \)
  - \( bound(\neg W)=bound(W) \)
- Binary connectives \( \land,\lor,\Rightarrow,\iff \):
  - Binary connectives merge sets
  - \( free(W_1\land W_2)=free(W_1)\cup free(W_2) \)
  - \( bound(W_1\land W_2)=bound(W_1)\cup bound(W_2) \)
- Quantifiers \( \forall ,\exists \):
  - Quantifiers bind variables
  - \( free(\forall x W)=free(W)\setminus \{x\} \)
  - \( bound(\forall x W)=bound(W)\cup \{x\} \)
Classification of formula \( W \):
- Closed iff \( free(W)=\emptyset \)
  - Constant truth value
  - Depend on the interpretation
- Open iff \( free(W)\neq \emptyset \)
  - Truth value depends on free variables (‌parameters)
Rectification:
- Bound variables are only valid within their scope
- Variable can be free and bound at the same time (but independent)
- Problem: Confusion
- Rectification: Rename variables
- \( W \) is rectified iff \( free(W) \cap bound(W) = \emptyset \)
Closures:
- Closure operation: Quantify/bind all free variables
- \( free(W)=\{x_1,\ldots,x_n\} \)
- Universal closure: \( \forall x_1,\ldots,x_n(W) \)
- Existential closure: \( \exists x_1,\ldots,x_n(W) \)

../_images/02-syntax.png

Semantics¶

Assumption:
- Formula is syntactically correct
- Meaning of symbols is considered common sense (e.g., 5 means 5, \( \land \) means AND)
Now: Interpretation of a language (and therefore statements)
- Give meaning to the symbols of the syntax
- Meaning of words/symbols?
- Which values can variables have?
Interpretation:
- Assigns an element of some Universe of Discourse to each term
- Assigns truth value to each formula (which statements are false/true)
- Capture the semantics of a language
Universe of Discourse:
- Non-empty set of objects, entities and concepts
- Contains entities/concepts related to our current application
- e.g., subset of real world

Interpretation¶

Interpretation of Language \( \mathcal{L} \)
- \( I_\mathcal{L}=(U, I_C, I_F, I_P) \)
\( U \):
- Universe Of Discourse
- All real objects, entities, concepts
- These are not just symbols or names
\( I_C \):
- \( I_C: \Gamma\rightarrow U \)
- Mapping of constants to the universe of discourse
- e.g., 5 is the natural number 5
\( I_F \):
- Mapping of function symbols to real functions
- \( I_F(f_n): U^n\rightarrow U \)
- e.g., + means addition
\( I_P \):
- Mapping of predicate symbols to real predicates
- \( I_P(R)\subseteq U^n \)
- e.g., Frog(x) means the type frog from the real world

Variable Substitution¶

\( \rho: X\rightarrow U \)
Assign to each variable a value of the universe of discourse

Term Evaluation¶

Each term \( t\in T_\mathcal{L} \) can be interpreted w.r.t.
- (1) an interpretation \( I_\mathcal{L} \) and
- (2) a variable substitution \( \rho \)
Term evaluation
- \( I^*_\rho(t) = t_I\in U \)
- \( t_I \) is the result of the interpretation of \( t \)
Informal:
- If term is a constant, use the constant interpretation
- If term is a variable, look up the variable substitution
- If term is a function, evaluate the function
Definition of \( I^*_\rho(t) \):
- \( t\in \Gamma \Rightarrow t_I=I_C(t) \) (constant)
- \( t\in X \Rightarrow t_I=\rho(t) \) (variable)
- \( t=f(t_1,\ldots,t_n)\Rightarrow t_I=I_F(f)(I^*_\rho(t_1),\ldots,I^*_\rho(t_n)) \) (function of terms)

Formula Evaluation¶

Formula evaluation \( I_\rho: F_\mathcal{L} \rightarrow \{\text{true},\text{false}\} \)
Assumptions
- Closed World Assumption
  - “Anything not mentioned in the universe of discourse does not exist”
  - Something not appearing in the predicate interpretation evaluates to false
- Open World Assumption:
  - Assume UoD is incomplete
  - Formulas may be evaluate to unknown
  - Problem: Difficult for KBS because a system answering unknown is not very useful
Variable substitutions
- Term evaluation does not assign truth values
- Question: For which substitutions is a formula true?
- Start of Logic programming, e.g., PROLOG

Atomic Formula¶

Atomic formula \( W=S(t_1,\ldots,t_n) \)
\( I_\rho(W)=\text{true}\iff I_\rho^*(t_1),\ldots,I_\rho^*(t_n)\in I_P(S) \)
Using closed world assumption

Non-atomic Formula¶

Use sub-formulas to evaluate concatenated formulas
Interpreting connectives:
- Connective is a boolean, binary function (defined by truth tables)
- \( I_\neg, I_\land, I_\lor, I_\Rightarrow, I_\Leftrightarrow \)
Definition of \( I_\rho:F_\mathcal{L} \)
- \( I_\rho(\neg W)=I_\neg(I_\rho(W)) \)
- \( \theta\in\{\land,\lor,\Rightarrow,\Leftrightarrow\}:I_\rho(W_1\,\theta\,W_2)=I_\theta(I_\rho(W_1),I_\rho(W_2)) \)

Quantified Formula¶

Requires modified substitutions
- Goal: Modify values of a substitution
- \( I_{\rho(x|d)}, x\in X, d\in U \)
- Substitute variable \( x \) with element \( d \), the remaining variables are unchanged
Idea:
- Formulae \( \exists x(W) \) or \( \forall x(W) \)
- Un-bind variable \( x \) and change its value using a modified substitution until the formula \( W \) evaluate to either true or false
Particular quantification:
- \( \exists x(W) \) is true if there exists any element in the universe evaluating formula \( W \) to true
- \( I_\rho(\exists x(W)) = \text{true iff }\text{true}\in\{I_{\rho(x|d)}(W) \mid d\in U\} \)
- Using closed world assumption (otherwise statement can not be interpreted)
Universal quantification:
- \( \forall x(W) \) is false if there exists any element in the universe evaluating formula \( W \) to false
- \( I_\rho(\forall x(W)) = \text{false iff }\text{false}\in\{I_{\rho(x|d)}(W) \mid d\in U\} \)
- Using closed world assumption (otherwise statement can not be interpreted)

Clauses¶

Definition Literal:
- Set of literals \( L_\mathcal{L} \) consists of all atomic formulae \( A\in A_\mathcal{L} \) and \( \neg \)
- Positive literal: \( A \)
- Negative literal: \( \neg A \)
- Ground literal: No variable in literal
Definition Clause:
- A clause is the Universal closure of a disjunction of literals
- e.g., \( \forall L_i\in L_\mathcal{L}:L_1\lor\ldots\lor L_n \)
Definition Horn clause:
- A Horn clause is a clause with at most a single positive literal
  - e.g., \( \forall (\neg L_1\lor\ldots\lor L_n) \)
- Definition Goal clause:
  - Horn clause without a positive literal
  - e.g., \( \neg A_1 \lor \neg A_2 \)
- Definition Definite clause:
  - Horn clause exactly one positive literal
  - e.g., \( \neg A_1 \lor A_2 \)
- Definition Fact clause:
  - Horn clause with exactly one positive literal and no negative literals
  - e.g., \( A \)
Horn clause as implication
- \( \neg A_1\lor A_2\equiv A_1\implies A_2 \)
- A set of preconditions follows one fact (required for deductive databases)

Models¶

Important question: Which interpretation and variable substitution make a formula true?
- Problem: Unlimited possible interpretations and variable substitutions
- Restriction: Use closed formulae
  - Variable substitution function irrelevant
  - Only rely on quantifiers
Definition Model:
- Interpretation \( I \) is a model of a closed formula \( W \) iff \( I_\rho(W)=I(W)=true \)
- \( I \) is model of a set of closed formulae \( \mathcal{W} \) iff it is a model for every \( W\in\mathcal{W} \)
Definition Fact:
- Closed formula \( W \) is a fact w.r.t. an interpretation \( I \) if \( I(W)=true \)

Satisfiability¶

Question: Does a set of closed formulae \( \mathcal{W} \) have a model?
Definition Satisfiable
- \( \mathcal{W} \) is called satisfiable iff \( \mathcal{W} \) has a model
- \( \mathcal{W} \) is called unsatisfiable iff \( \mathcal{W} \) does not have any model
- Stop evaluation of an unsatisfiable set
- Check for unsatisfiability is easier (really?)
Connection between satisfiability of a set of formulae and inference:
- To infer formulae, we must check for satisfiability
- Principle of indirect proof by Aristotle (reductio ad absurdum)
- Goal: Prove \( W \) using set of propositions \( \mathcal{W} \)
- Assume: \( \neg W \)
- Show contradiction to some statement in \( \mathcal{W} \)
- Thus, \( \mathcal{W}\cup \{\neg W\} \) is unsatisfiable
\( \mathcal{W}\models W \iff \mathcal{W}\cup \{\neg W\} \text{ is unsatisfiable} \)

../_images/04-classes.png

Semantic Equivalence¶

Question: Describe two concepts the same idea? (redundant rules waste time/space)
Definition:
- \( W_1 \) and \( W_2 \) are semantically equivalent iff \( \forall I: I(W_1)=I(W_2) \)
- Evaluation of both formulae is always the same
Can be derived by using tautologies as transformation rules

Semantic Conclusion¶

Question: Can a certain fact be deduced from a given set of facts?
Trade-off:
- Query time vs. size of the IDB
- i.e., store rule (so no conclusion must be drawn) or calculate rule at query time
Definition:
- \( W \) is semantic conclusion of \( \mathcal{W} \) iff every model of \( \mathcal{W} \) is also a model of \( W \)
- Notation: \( \mathcal{W}\models W \) (\( W \) follows from \( \mathcal{W} \)

Tautology¶

Class of formulae
Every single interpretation is a model
Definition universal:
- \( \mathcal{W} \) is universal if every interpretation is a model
- Notation: \( \models \mathcal{W} \)
Definition Tautology
- \( \mathcal{W} \) is a tautology if it is a universal
Use the set of all tautologies to derive semantic equivalences (tautologies as transformation rules)
Examples
- \( W\lor\neg W \)
- \( W_1\land W_2\implies W_1 \)
- \( W\equiv \neg\neg W \)

Test for Unsatisfiability¶

Use Case:
- When the user adds a formula, check if the formula is semantically equivalent or a contradiction
  - Redundancy: \( \mathcal{W}\equiv W \)
  - Contradiction: \( \mathcal{W}\cup \{W\} \) unsatisfiable
Lemma:
- \( \mathcal{W}\models \neg W \iff \mathcal{W}\cup \{W\} \text{ is unsatisfiable} \)
- Statement and contradiction can not be true at the same time
The Test:
1. Test \( \mathcal{W}\cup\{W\} \) is unsatisfiable
2. [Lemma]: Test \( \mathcal{W}\models \neg W \)
3. [Definition]: Every model of \( \mathcal{W} \) must be a model \( \neg W \)
4. [model-theoretical approach]: Test all possible interpretations to find a model
5. [Problem]: Unlimited amount of interpretations (leads to Herbrand Theory)
6. [Herbrand Model]: Find a Herbrand Model of \( \mathcal{W} \) (only for clauses)
7. [Herbrand Theorem]: Find a Herbrand Expansion not satisfying \( \neg W \) (using Boolean Logic)
Problem: Unlimited amount of interpretations
Solution:
- Use interpretations which are representative for the entire class of all interpretations (e.g., natural numbers, even numbers)
- Restrict to clauses and use Herbrand interpretations
Problem: Approach is theoretical
- This test for unsatisfiability can not be implemented
- In deductive databases, the bottom-up approach is used
- i.e., compute the transitive hull of \( \mathcal{W} \) and test if the formula is satisfiable

Herbrand Theory¶

Goal:
- Define a representative interpretation which can replace any other (so-called Herbrand Interpretation)
- Provide a reduction of first-order logic to propositional logic (only works for clauses)
Given a language \( \mathcal{L} \)
Herbrand interpretation consists of two parts:
- Herbrand Universe \( U_\mathcal{L} \)
  - Consists of all ground terms
  - Only use constants and functions, no variables
- Herbrand Base \( B_\mathcal{L} \)
  - Contains all ground atoms, i.e., no variables
  - ‌Take all the terms of the Herbrand universe and apply the predicates of the language \( \mathcal{L} \) to them
  - Infinite set
  - \( P(t_1,\ldots,t_n)\subseteq B_\mathcal{L} \) with \( t_i\in U_\mathcal{L} \)

Herbrand Interpretation¶

Definition
- \( I=(U,I_C,I_F,I_P) \)
- \( U=U_\mathcal{L} \) (Herbrand Universe)
- \( I_C(c)=c \) (interprete by itself)
- \( I_F(f):U_\mathcal{L}^n\rightarrow U_\mathcal{L}, f(t_1,\ldots,t_n)\mapsto f(t_1,\ldots,t_n) \) (interprete by itself)
‌Completely symbolic/syntactical interpretation without a specific real-world semantics
- Term \( f(x) \) has no meaning (just a symbol)
- Universe element \( f(x) \) is interpreted (meaning)
Difference between multiple Herbrand Interpretations:
- \( U, I_C, I_F \) are always the same
- Only difference:
  - Predicate Interpretation \( I_P \)
- Idea:
  - Define a Herbrand interpretation only by listing the atoms which evaluate to true and all others are false
- Interpretation is defined by the subset of the Herbrand Base \( I\subseteq B_\mathcal{L} \)
- Results in Closed World Assumption (everything not mentioned is false)

Herbrand Model¶

Definition
- A Herbrand model of a set of formulae \( \mathcal{W} \) is a Herbrand interpretation which is a model \( \mathcal{W} \)
Example:
- Formula: \( W\equiv\forall x,y(loves(x,y)\implies loves(y,x)) \)
- \( I_1=\{loves(Tarzan, Jane), loves(Jane, Tarzan)\} \) is a Herbrand Model
- \( I_2=\{loves(Tarzan, Jane), loves(Jane, Paul)\} \) is not a Herbrand Model
Lemma:
- Given set of clauses \( \mathcal{W} \)
- \( \mathcal{W} \) has model if and only if \( \mathcal{W} \) has a Herbrand model
- \( \mathcal{W} \) is unsatisfiable if and only if \( \mathcal{W} \) has no Herbrand model
- Meaning: Syntactical interpretation of all symbols
- Idea:
  - If some syntactical interpretation can satisfy the set of clauses, there is some semantic interpretation (more or less useful)
Test for Unsatisfiability:
- see above
- Instead of testing all models of \( \mathcal{W} \), only show the (non-)existance of a single Herbrand model
- Only works for clauses not for general closed formulas

Complexity (D)¶

Use Case:
- Deductive DB checks if a given statement can be deduced from a given set of formulae
- Check \( \mathcal{W}\models W \) (\( \mathcal{W}\cup\{W\} \))
Focus: Computational complexity (for databases this is important)
- Check for validity (tautology)
- Check for satisfiability
Sets of expressions:
- VALID (tautology)
  - \( \models W \)
- SATISFIABLE (but not valid)
- UNSATISFIABLE
- Negation as mirror operation
Check for classes:
- Satisfiable: Generate substitution, evaluate
- \( W \) valid: Check if \( \neg W \) is unsatisfiable
- \( W \) unsatisfiable: Check if \( W \) is satisfiable
Satisfiability:
- Propositional logic: Decidable
- First-order logic: Undecidable

../_images/04-3-classes.png

Propositional Logic¶

SAT problem:
- ‌Satisfiability problem
- Is a given propositional formula satisfiable?
Complexity class: NP-C

SAT Algorithms¶

Deterministic decidable algorithm
- Generate all \( 2^n \) substitutions
- Evaluate all substitutions (\( O(n^2) \) per substitution)
- Overall \( O(n^2 2^n) \)
Non-deterministic semi-decidable algorithm
- Guess any substitution
- Evaluate this substitution (\( O(n^2) \))
- Continue until the evaluation is \( true \)
Construct a substitution
- Idea: Construct a substitution using the formula
- e.g., one variable must be true and one has to be false
- i.e., exclude certain substitutions
- Problem: Hard for general formulae
Davis-Putnam Algorithm
- Default algorithm to solve SAT
- Formula must be in conjunctive normal form
- \( O(1.8^n) \)
- Idea: Build a pruned tree of possible substitutions

SAT Variants¶

3-SAT
- Formula must be conjunctive normal form where each clause contains at most 3 literals
- First problem shown to be NP-complete
- SAT reduces polynomially to 3-SAT
Horn-SAT
- SAT with conjunctive normal form where each clause is a Horn clause
- Important: P-complete
- Idea:
  - Write Horn clause in implication form
    - Facts: \( true\rightarrow x_1 \)
    - Definites: \( x_1\rightarrow x_2 \)
    - Goals: \( x_1\land x_2\rightarrow false \)
  - A set of Horn clauses is satisfiable iff all conjunctions of implications is true
  - Find variables which have to be true
- Algorithm:
  1. Set \( T=\emptyset \) contains all variables which must be true (all others are false)
  2. Pick any (currently) unsatisfied/false implication
    - \( H_i\equiv\bigwedge x_j\Rightarrow y \)
    - Must be a fact or a definite
  3. Add \( y \) to \( T \): \( T=T\cup \{y\} \)
  4. Repeat, until no unsatisfied/false implications exist
  5. Result: Iff \( T \) satisfies all clauses, \( \mathcal{W} \) is satisfiable

First-Order Logic¶

Problem:
- Universe of potentially unlimited size (interpretations)
- Quantifiers (formula must be true for subset of universe)

Example (Number Theory)¶

Language
- \( \mathcal{L}_{NT}=(\{0\}, \{\sigma, +,\times, \uparrow\}, \{=,<\},\{x,y,z\}) \)
Interpretation
- Universe: All natural numbers
- Successor function \( \sigma \):
  - \( \sigma(\sigma(\sigma(0)))=3 \)
  - Shortcut: Decimal numbers
- Functions and functions are interpreted common sense
Naive evaluation: Testing all values is very problematic
- e.g., \( \exists x(x>2000) \)
Problem:
- Testing for all possible substitutions in an infinite universe does not work

Peano Arithmetic¶

Guiseppe Peano, 1889
Idea:
- Use deductive system to construct a proof (from a set of valid axioms)
- Do not test all possible values
Axiomatization of Number Theory
- 15 axiom types inducing countable unlimited number of axioms

Fermats Last Theorem¶

\( \neg\exists n,a,b,c((a^n+b^n=c^n\land n>2) \)
Took very long (357 years) to show that this statement is provable for the natural numbers
1995: Proved by Andrew Wiles

Gödel’s Incompleteness Theorem¶

[…] generated theory can not be both consistent and complete. […]
e.g., some statements are provable in the Peano arithmetic (Goodstein Theorem and Fermats Last Theorem)
Result:
- For any non-trivial deductive system \( NT \), there exists a statement, which can not be proved within this system
Unprovable is called undecidable
\( NT\vdash W \): \( W \) can be proved in system \( NT \)
Note:
- First-order logic can not be used to model infinite domains (e.g., the natural numbers)
- Hence, the incompleteness theorem does not apply to FOL

../_images/04-classes.png

Goodstein Theorem¶

Statement about the natural numbers (Hercules fighting the Hydra)
Goodstein sequence eventually terminates at 0
\( Goodstein(3)=3,3,3,2,1,0 \)
\( Goodstein(4)=4,26,41,\ldots,299,\ldots,0 \)
Theorem is expressible and true in the Peano arithmetic

Paris-Kirby Theorem¶

Goodstein Theorem is not decidable
Can not be proven in Peano Arithmetic (or First-Order Logic)
Why?
- Consistency of Peano arithmetic would follow from the proof of the Goodstein Theorem
- This is not possible due to Gödel’s incompleteness Theorem (Peano arithmetic can not prove its consistency)

Herbrand Theorem¶

Jacques Herbrand, 1928
Informal:
- Closed formula \( A \) in universal prenex form is unsatisfiable iff there is a finite subset of the Herbrand expansion of \( A \) \( TA\subseteq E(A) \) which is Boolean unsatisfiable
Result:
- Transform the First-Order Logic satisfiability problem to the Propositional Logic Satisfiability Problem (using this restriction)
- By assigning a truth value to each predicate in a ground instance the formula represents a propositional logic formula

Formalization¶

Universal prenex form:
- Prefix: Universal Quantifier binding all variables
- Matrix: Formula without quantifiers
- \( \forall y_1,\ldots,y_n (F(y_1,\ldots,y_n)) \)
- \( F \) is quantifier-free
Instance of \( A \):
- Formula where variables of \( A \) are substituted by entities
‌Herbrand expansion \( E(A) \):
- Set of all possible ground instances of \( A \) with all substitutions from the Herbrand base
Herbrand Theorem:
- \( A\equiv\forall y_1,\ldots,y_n(F(y_1,\ldots,y_n)) \)
- \( A \) is unsatisfiable if and only if there is a finite set \( TA\subseteq E(A) \) of ground instances such that \( TA \) is unsatisfiable
Considerations:
- Check of \( TA \) can be performed in finite time
- e.g., Davis-Putnam algorithm
- Problem: Which \( TA\subseteq E(A) \) is unsatisfiable?
  - Reducing to the Halting problem

Gilmore Algorithm¶

1960
Meta-algorithm to check for unsatisfiability
Algorithm:
- Input:
  - FOL formula \( A \)
  - Transform to universal prenex form (i.e., pull quantifiers and convert to universal quantifier)
- Criterion:
  - Herbrand Expansion must be generateable (i.e., recursively enumerable)
  - i.e., \( E(A)=\{A_1,A_2,\ldots\} \)
- \( k:=1 \)
- WHILE \( \bigwedge_{i=1}^k A_i \) is satisfiable: k++ (while not unsatisfiable)
- RETURN 'A unsatisfiable'
Semi-decidable algorithm (only terminates if \( A \) is unsatisfiable)

Schönfinkel-Bernays Class¶

Restriction: Allow only a decidable subset of formulae
Schönfinkel-Bernays class
- No functional symbols
- No equality predicate
- Formula \( W \) in prenex form
SB-SAT:
- Satisfiability of formulae of SB-class is decidable
Proof:
- No functional symbols
- –> Finite Herbrand Base
- –> Finite Herbrand Expansion
- –> Generation in finite time
- –> Finite time for the unsatisfiability check
Problem:
- SB-SAT is in NEXP-C
- NEXP: Non-deterministic exponential time algorithm
- No functional symbols (restricts expressiveness)

Restriction¶

Do we need full First-Order Logics?
Requirements:
- Subset of FOL with guaranteed finite Herbrand expansions
- Better complexity than NEXP
- Subset should not limit expressiveness
Restriction:
- Restrict to Horn clauses
  - Finite Herbrand universe
  - Check is in P
- Restrict to Non-recursive typed functions
Advantage:
- Check for unsatisfiability of finite subsets of Herbrand expansion is in \( PTIME \)

Deductive Systems (D)¶

Question: How to find the set of all tautologies?
- Find the universal truth
- Automatically proof theorems
Approaches:
- Model-theoretical (this course)
  - Bottom-up approach (find a Herbrand model)
- Proof-theoretical
  - Hilbert-Style deduction system
  - Natural deduction
David Hilbert
- Mathematician in Göttingen (also university of Gauss and Riemann)
- Königsberg, 1862
- Pioneer in proof theory and logics
The Hilbert Program
- Started in 1920
- Goal: Completely formalize math to finite, complete set and axioms
  - Preciseness: Use precisely defined formalisms
  - Completeness: All math can be proved by a system
  - Consistency: No contradictions will show up
  - Decidability: For each statement, an algorithm can decide if it is true
- Gödel incompleteness theorem:
  - Prove that the Hilbert Program is impossible

Deduction Theorem¶

\( \mathcal{W}\cup\{W_1\}\models W_2\iff \mathcal{W}\models W_1\implies W_2 \)
Fundamental Meta-Rule: Deduction theorem is considered true in every system but not a theorem of that system
Inference rules:
- Modus Ponens (Implication Elimination Rule)
- Abduction Inference Rule

Modus Ponens¶

‌Implication Elimination Rule
\( \{W_1, W_1\implies W_2\}\models W_2 \)
Sound, i.e., never generates incorrect knowledge
Example (for not-sound):
- Fact \( W_1 \): Today is Tuesday
- Rule \( W_1\implies W_2 \): If today is Tuesday, today is KBS lecture
- Derived \( W_2 \): Today is KBS lecture
Usually sufficient for axiomatic systems

Abduction Inference Rule¶

\( \{W_1\implies W_2, W_2\}\models W_1 \)
Not sound
Often helpful, used in medicine
Example:
- Rule \( W_1\implies W_2 \): If it rains, it is wet
- Fact \( W_2 \): It is wet
- Derived \( W_1 \): It has rained

Hilbert-Style Deduction System¶

Deduction System: Logic
Also called Axiomatic systems
Hilbert-style deduction system for a language \( \mathcal{L} \)
Components:
- Logical axioms
  - Set of formulae of \( \mathcal{L} \)
  - Can not be proven that they are true/false
- Inference rules
  - Set of rules to transform one statement to another
Deduction System generates proofs
Axiom must be an instance of the following schemes:
- A1: \( A\Rightarrow(B\Rightarrow A) \)
- A2: \( (A\Rightarrow (B\Rightarrow C))\Rightarrow((A\Rightarrow B)\Rightarrow(A\Rightarrow C)) \)
- A3: \( (\neg A\Rightarrow\neg B)\Rightarrow(B\Rightarrow A) \)
- All axioms are tautologies
- There is an unlimited number of axioms
Proof from \( \mathcal{W} \) to \( A \):
- Finite sequence \( W_1,\ldots,W_n \) of formulae of \( \mathcal{L} \) such that \( W_i \) is either an axiom or follows from one of the previous \( W_j \) by the inference rules
Example:
- Prove: \( \models \neg B\Rightarrow (B\Rightarrow A) \)
1. \( \neg B\models B\Rightarrow A \) (Deduction theorem)
2. \( \neg B \) (Hypothesis)
3. \( \neg B\Rightarrow (\neg A\Rightarrow\neg B) \) (Axiom 1)
4. \( \neg A\Rightarrow\neg B \) (Modus Ponens)
5. \( (\neg A\Rightarrow\neg B)\rightarrow(B\Rightarrow A) \) (Axiom 3)
6. \( B\rightarrow A \) (Modus Ponens)
Drawbacks:
- Few rules but many axioms (contradicts goals of deductive databases)
- Finding proofs is tricky (trial and error)
- Feels unnatural

Natural Deduction¶

Gerhard Gentzen, 1938
Use more rules but a limited set of axioms
Later been adapted to deductive databases
Concepts:
- Axioms (tautologies)
- Logical rules
- Structural rules (syntactical)